variable A : Type
variables x y z : A
variable P : A → Prop
example : x = x :=
show x = x, from eq.refl x
example : y = x :=
have h : x = y, from sorry,
show y = x, from eq.symm h
example : x = z :=
have h1 : x = y, from sorry,
have h2 : y = z, from sorry,
show x = z, from eq.trans h1 h2
example : P y :=
have h1 : x = y, from sorry,
have h2 : P x, from sorry,
show P y, from eq.subst h1 h2