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