proposition: Lemma confluence_par_red : str_confluent par_red.
proof: Proof. red in |- *; red in |- *. simple induction 1; intros. elim strip_lemma with z x0 y0; intros; auto with coc core arith sets. exists x1; auto with coc core arith sets. elim H1 with z0; intros; auto with coc core arith sets. elim H3 with x1; intros; auto with coc core arith sets. exists x2; auto with coc core arith sets. red in |- *. apply t_trans with x1; auto with coc core arith sets. Qed.
imports: Termes