fact: Fixpoint path_nat {n m} : (n =n m) -> (n = m) := match m as m, n as n return (n =n m) -> (n = m) with | 0, 0 => fun _ => idpath | m'.+1, n'.+1 => fun H : (n' =n m') => ap S (path_nat H) | _, _ => fun H => match H with end end.
imports: Basics Types Basics.Nat HoTT.DProp