proposition: Theorem inject_of_finite (n : nat): inject (\F n) = n.
proof: Proof. destruct n. - apply inject_of_zero. - apply inject_of_finite_pos. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)