fact: Definition two_rec {A : UU} (a b : A) : ⟦2⟧ -> A.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions