proposition: Lemma str_confluence_par_red1 : str_confluent par_red1.
proof: Proof. red in |- *; red in |- *. simple induction 1; intros. inversion_clear H4. elim H1 with M'0; auto with coc core arith sets; intros. elim H3 with N'0; auto with coc core arith sets; intros. exists (subst x1 x0); unfold subst in |- *; auto with coc core arith sets. inversion_clear H5. elim H1 with M'1; auto with coc core arith sets; intros. elim H3 with N'0; auto with coc core arith sets; intros. exists (subst x1 x0); auto with coc core arith sets; unfold subst in |- *; auto with coc core arith sets. inversion_clear H0. exists (Srt s); auto with coc core arith sets. inversion_clear H0. exists (Ref n); auto with coc core arith sets. inversion_clear H4. elim H1 with M'0; auto with coc core arith sets; intros. elim H3 with T'0; auto with coc core arith sets; intros. exists (Abs x1 x0); auto with coc core arith sets. generalize H0 H1. clear H0 H1. inversion_clear H4. intro. inversion_clear H4. intros. elim H4 with (Abs T M'0); auto with coc core arith sets; intros. elim H3 with N'0; auto with coc core arith sets; intros. apply inv_par_red_abs with T' M'1 x0; intros; auto with coc core arith sets. generalize H7 H8. rewrite H11. clear H7 H8; intros. inversion_clear H7. inversion_clear H8. exists (subst x1 U'); auto with coc core arith sets. unfold subst in |- *; auto with coc core arith sets. intros. elim H5 with M'0; auto with coc core arith sets; intros. elim H3 with N'0; auto with coc core arith sets; intros. exists (App x0 x1); auto with coc core arith sets. intros. inversion_clear H4. elim H1 with M'0; auto with coc core arith sets; intros. elim H3 with N'0; auto with coc core arith sets; intros. exists (Prod x0 x1); auto with coc core arith sets. Qed.
imports: Termes