proposition: Lemma inject_rw (a b: T1) n : inject (T1.cons a n b) = mult_Sn (AP._phi0 (inject a)) n + inject b.
proof: Proof. reflexivity. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)