proposition: Lemma folds_iso_implies_E (C : folds_pre_2_cat) (a b : C) (f g : a ⇒ b) : folds_iso f g → E f g.
proof: Proof. intro Isofg. set (keytojoy := pr1 (pr2 (pr2 (pr2 Isofg)))). apply (keytojoy f). set (H' := pr2 (pr2 (pr1 C))). simpl in H'. destruct H' as [[[Erefl Esym] Etrans] [EI ET]]. apply Erefl. Qed.
imports: UniMath.Folds.UnicodeNotations UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets