** Module lib_eq Imports lib_logic $Eq : {t|Type}t->t->Prop $Eqr : {t|Type}{x:t}Eq x x $Eq_elim : {t|Type}{P:{x,y:t}(Eq x y)->Type}({x:t}P x x (Eqr x))->{x,y:t} {p:Eq x y}P x y p [[t:Type][P:{x,y:t}(Eq x y)->Type][h:{x:t}P x x (Eqr x)][x:t] Eq_elim P h x x (Eqr x) ==> h x] Eq_refl = ... : {t|Type}refl (Eq|t) Eq_subst = ... : {t|Type}{m,n|t}(Eq m n)->{P:t->Type}(P m)->P n trivType = ... : Type emptyType = ... : Type ** Config Theorems trivType emptyType Eq_subst