proposition: Remark R3 : Forall (fun beta => beta < alpha) l.
proof: Proof. unfold l; constructor. apply lt_succ_lt. unfold alpha. apply is_limit_phi0. auto with schutte. apply R1. constructor. Qed.
imports: hydras(Schutte AP CNF) Coq(List)