proposition: Lemma strip_lemma : commut _ par_red (transp _ par_red1).
proof: Proof. unfold commut, par_red in |- *; simple induction 1; intros. elim str_confluence_par_red1 with z x0 y0; auto with coc core arith sets; intros. exists x1; auto with coc core arith sets. elim H1 with z0; auto with coc core arith sets; intros. elim H3 with x1; intros; auto with coc core arith sets. exists x2; auto with coc core arith sets. apply t_trans with x1; auto with coc core arith sets. Qed.
imports: Termes