2014-12-16 13:28:43 -08:00
|
|
|
open eq
|
|
|
|
|
|
|
|
|
|
definition concat_pV_p {A : Type} {x y z : A} (p : x = z) (q : y = z) : (p ⬝ q⁻¹) ⬝ q = p :=
|
|
|
|
|
begin
|
|
|
|
|
generalize p,
|
2015-05-01 15:07:28 -07:00
|
|
|
eapply (eq.rec_on q),
|
2014-12-16 13:28:43 -08:00
|
|
|
intro p,
|
|
|
|
|
apply (eq.rec_on p),
|
|
|
|
|
apply idp
|
|
|
|
|
end
|
