proposition: Lemma confluence_Epar_red : str_confluent Epar_red.
proof: Proof. red in |- *; red in |- *. simple induction 1; intros. elim strip_lemma_Epar_red1 with z x0 y0; intros; auto with ecoc coc core arith sets. split with x1; auto with ecoc coc core arith sets. elim H1 with z0; intros; auto with ecoc coc core arith sets. elim H3 with x1; intros; auto with ecoc coc core arith sets. split with x2; auto with ecoc coc core arith sets. red in |- *; apply t_trans with x1; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv