proposition: Theorem inject_plus (alpha beta : T1): nf alpha -> nf beta -> inject (alpha + beta)%t1 = inject alpha + inject beta.
proof: Proof. Proof with eauto with T1. induction alpha. - simpl; now rewrite zero_plus_alpha. - intros H H0; destruct beta. + simpl (inject (T1.cons alpha1 n alpha2)); rewrite <- plus_assoc; simpl (inject T1.zero); now rewrite alpha_plus_zero. + repeat rewrite inject_rw. simpl. destruct (compare alpha1 beta1) eqn:H1; repeat rewrite inject_rw. * apply compare_eq_iff in H1 as <-. rewrite <- (case_Eq (inject alpha1) (inject alpha2) (inject alpha1) (inject beta2) n n0) ... -- assert (H1 : (alpha2 t1< T1.phi0 alpha1)%t1). { rewrite nf_LT_iff in H; tauto. } rewrite <- inject_of_phi0. apply inject_mono ... -- rewrite <- inject_of_phi0; apply inject_mono ... rewrite nf_LT_iff in H0 ... decompose [and] H0 ... * rewrite compare_lt_iff in H1. { repeat rewrite inject_rw; rewrite case_lt; auto. rewrite <- inject_of_phi0; apply inject_mono ... - rewrite nf_LT_iff in H; decompose [and] H ... - apply inject_mono; eauto with T1. } * rewrite compare_gt_iff in H1. repeat rewrite inject_rw; rewrite case_gt. f_equal; rewrite IHalpha2 ... Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)