next up previous contents
Next: Setoids Up: Equality Previous: Martin-Löf's Inductive Equality

Altenkirch-Streicher Elimination Rule

This file contains an extra elimination rule for Martin-Löf's inductive equality proposed by Thorsten Altenkirch and Thomas Streicher. This new rule is used to prove the proposition Eq_unique below which allows one to prove e.g. that equality in inductive sigma types respects second projection. This rule has recently been shown not to be derivable from the usual elimination rule for inductive equality.

 ** Module lib_AS_eq Imports lib_equality/ML/lib_eq
 $Eq_elim' :
    {A|Type}{C:{a|A}(Eq a a)->Type}({a:A}C (Eq_refl a))->{a|A}{p:Eq a a}
    C p
* Eq_unique = ... : {A|Type}{a,b:A}{p,q:Eq a b}Eq p q

Fri May 24 19:01:27 BST 1996