proposition: Lemma strip_lemma_Epar_red1 : commut _ Epar_red (transp _ Epar_red1).
proof: Proof. unfold commut, Epar_red in |- *; simple induction 1; intros. elim str_confluence_Epar_red1 with z x0 y0; auto with ecoc coc core arith sets; intros. split with x1; auto with ecoc coc core arith sets. elim H1 with z0; auto with ecoc coc core arith sets; intros. elim H3 with x1; intros; auto with ecoc coc core arith sets. split with x2; auto with ecoc coc core arith sets. apply t_trans with x1; auto with ecoc coc core arith sets. Qed.
imports: Termes Conv