Module id Import pred;

$[Id : {X|Set}X -> X -> Prop];
$[refl : {X|Set}{x:X}Id x x];
$[subst : {X|Set}{P:X->Prop}{x,y|X}
		(Id x y)->(P x)->(P y)];

[[X:Set][P:X->Set][x:X][p:P x]
   subst P (refl x) p ==> p];

Goal {A|Set}{a,b|A}(Id a b)->(Id b a);
Intros A a b p;
Refine subst ([b:A]Id b a) p;
Refine refl;
Save symId;

Goal {A|Set}{a,b,c|A}(Id a b)->(Id b c)->(Id a c);
Intros A a b c p q;
Refine subst ? q;
Refine p;
Save transId;

Goal {A,B|Set}{f:A->B}{a,b|A}(Id a b)->(Id (f a) (f b));
Intros;
Refine subst ([x:A]Id (f a) (f x));
Next +1;
Refine H;
Refine refl;
Save respId;