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