proposition: Lemma E_transport_source : ∏ (C : folds_pre_2_cat) (a a' b : C) (f g : a ⇒ b) (p : a = a'), E f g → E (transportf (λ c, c ⇒ b) p f) (transportf (λ c, c ⇒ b) p g).
proof: Proof. intros. destruct p. assumption. Defined.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets