i \le n \to j \le n \to f i = f j \to i = j.
theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
i \le n \to j \le n \to f i = f j \to i = j.
theorem injn_Sn_n: \forall f:nat \to nat. \forall n:nat.
apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
apply (H2 O ? ? (S(m1+i))).
apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
apply (trans_eq ? ? (map_iter_i (S k) (\lambda m. g
(transpose i (S(m1 + i)) (transpose (S(m1 + i)) (S(S(m1 + i))) m))) f n)).
apply (H2 O ? ? (S(m1+i))).
apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
apply eq_map_iter_i.
intros.apply eq_f.
apply sym_eq. apply eq_transpose.
apply (trans_le ? (S(S (m1+i)))).
apply le_S.apply le_n.assumption.
apply eq_map_iter_i.
intros.apply eq_f.
apply sym_eq. apply eq_transpose.