fact: Fixpoint code_nat (m n : nat) {struct m} : DProp.DHProp := match m with | O => match n with | O => DProp.True | S _ => DProp.False end | S m' => match n with | O => DProp.False | S n' => code_nat m' n' end end.
imports: HoTT(Basics Types DProp Tactics.EquivalenceInduction)