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_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