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