proposition: Lemma concat_A1p_lemma {A} (f : A -> A) (p : forall x, f x = x) {x y : A} (q : x = y) : (concat_A1p p q) = (concat_A1p p q).
proof: Proof. apply_funelim (concat_A1p p q). clear; intros. simpl. elim Heq0 using Logic.Id_rect_r. simpl. reflexivity. Qed.
imports: Unicode.Utf8 Coq.Program.Tactics Setoid Relations Equations.Type.All CRelationClasses CMorphisms