fact: Definition concat2 {A} {x y z : A} {p p' : x = y} {q q' : y = z} (h : p = p') (h' : q = q') : p @ q = p' @ q' := match h, h' with 1, 1 => 1 end.
imports: Unicode.Utf8 Coq.Program.Tactics Setoid Relations Equations.Type.All CRelationClasses CMorphisms