proposition: Lemma inject_lt_epsilon0_ex_cnf (alpha : Ord) : forall (H : alpha < epsilon0) (l: list Ord), is_cnf_of alpha l -> exists t: T1, nf t /\ inject t = eval l.
proof: Proof. pattern alpha; apply well_founded_induction with (R:=lt). { exact all_ord_acc. } { clear alpha; intros alpha IHalpha H. destruct l. - exists T1.zero; simpl; unfold nf; split; auto. - inversion_clear 1. pose (H3 := IHalpha o). assert (H0 : o < alpha). { simpl in H2; subst alpha; apply lt_le_trans with (AP._phi0 o). - apply lt_phi0; apply le_lt_trans with (AP._phi0 o). + apply le_phi0. + apply le_lt_trans with (2:= H); apply le_plus_l. - apply le_plus_l. } assert (H4 : o < epsilon0). { apply lt_trans with alpha; auto. } specialize (H3 H0 H4); destruct (cnf_exists o) as [x H5]. specialize (IHalpha (eval l)). assert (H6 : eval l < alpha). { simpl in H2; subst alpha; apply sorted_lt; auto. } assert (H7 : eval l < epsilon0). { apply lt_trans with alpha; auto. } destruct (H3 _ H5) as [x0 H8]. destruct H8 as [H8 H9]; specialize (IHalpha H6 H7). + destruct (IHalpha l). * split; trivial. eapply sorted_tail; eauto. * destruct H10 as [H10 H11]; exists (T1.phi0 x0 + x1)%t1. split. -- apply plus_nf ; eauto with T1. -- simpl eval; rewrite <- H11; rewrite inject_plus; auto with T1. simpl (inject (T1.phi0 x0)); rewrite H9; destruct H5. rewrite <- H12; rewrite alpha_plus_zero; auto. } Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)