proposition: Lemma confluence_red : str_confluent red.
proof: Proof. red in |- *; red in |- *. intros. elim confluence_par_red with x y z; auto with coc core arith sets; intros. exists x0; auto with coc core arith sets. Qed.
imports: Termes