proposition: Lemma str_confluence_Epar_red1 : str_confluent Epar_red1.
proof: Proof. red in |- *; red in |- *. simple induction 1; intros. inversion_clear H4. elim H1 with M'0; auto with ecoc coc core arith sets; intros. elim H3 with N'0; auto with ecoc coc core arith sets; intros. split with (subst x1 x0); unfold subst in |- *; auto with coc ecoc core arith sets. inversion_clear H5. elim H1 with M'1; auto with ecoc coc core arith sets; intros. elim H3 with N'0; auto with ecoc coc core arith sets; intros. split with (subst x1 x0); auto with ecoc coc core arith sets. unfold subst in |- *; auto with ecoc coc core arith sets. elim H1 with M'1; auto with ecoc coc core arith sets; intros. elim H3 with N'0; auto with ecoc coc core arith sets; intros. split with (subst x1 x0); auto with ecoc coc core arith sets. unfold subst in |- *; auto with ecoc coc core arith sets. inversion_clear H2. elim H1 with M'0; auto with ecoc coc core arith sets; intros. split with (Abs (Srt prop) x0); eauto with ecoc coc core arith sets; intros. elim H1 with M'0; auto with ecoc coc core arith sets; intros. split with (Abs (Srt prop) x0); eauto with ecoc coc core arith sets. inversion_clear H0. split with (Srt s); auto with ecoc coc core arith sets. inversion_clear H0. split with (Ref n); auto with ecoc coc core arith sets. inversion_clear H4. elim H1 with M'0; auto with ecoc coc core arith sets; intros. split with (Abs (Srt prop) x0); eauto with ecoc coc core arith sets. elim H1 with M'0; auto with ecoc coc core arith sets; intros. elim H3 with T'0; auto with ecoc coc core arith sets; intros. split with (Abs x1 x0); auto with ecoc coc core arith sets. generalize H0 H1. clear H0 H1. inversion_clear H4. intro. inversion_clear H4. intros. elim H4 with (Abs (Srt prop) M'0); auto with coc core arith sets; intros. elim H3 with N'0; auto with coc core arith sets; intros. apply inv_Epar_red_abs with (Srt prop) M'1 x0; intros; auto with coc core arith sets. rewrite H10 in H7; inversion_clear H7. split with (subst x1 U'); auto with ecoc sets. unfold subst in |- *; auto with ecoc coc core arith sets. split with (subst x1 U'); auto with ecoc sets. unfold subst in |- *; auto with ecoc coc core arith sets. auto with ecoc sets. intros. elim H3 with N'0; auto with ecoc sets; intros. elim H4 with (Abs T' M'0); auto with ecoc sets; intros. apply inv_Epar_red_abs with T' M'0 x1; intros; auto with coc core arith sets. rewrite H11 in H9; inversion_clear H9. split with (subst x0 U'); auto with ecoc sets. unfold subst in |- *; auto with ecoc coc core arith sets. split with (subst x0 U'); auto with ecoc sets. unfold subst in |- *; auto with ecoc coc core arith sets. intros. elim H5 with M'0; auto with ecoc sets; intros. elim H3 with N'0; auto with ecoc sets; intros. split with (App x0 x1); auto with ecoc sets. inversion_clear H4. elim H1 with M'0; auto with coc ecoc sets; intros. elim H3 with N'0; auto with coc ecoc sets; intros. split with (Prod x0 x1); auto with ecoc sets. Qed.
imports: Termes Conv