fact: Fixpoint weak {m}{n} p (f : t m -> t n) : t (p + m) -> t (p + n) := match p as p' return t (p' + m) -> t (p' + n) with |0 => f |S p' => fun x => match x with |@F1 n' => fun eq : n' = p' + m => F1 |@FS n' y => fun eq : n' = p' + m => FS (weak p' f (eq_rect _ t y _ eq)) end (eq_refl _) end.
imports: PeanoNat