proposition: Lemma Epar_red1_subst : forall c d : term, Epar_red1 c d -> forall a b : term, Epar_red1 a b -> forall k : nat, Epar_red1 (subst_rec a c k) (subst_rec b d k).
proof: Proof. simple induction 1; simpl in |- *; eauto with coc ecoc core arith sets; intros. rewrite distr_subst; auto with coc ecoc core arith sets. elim (lt_eq_lt_dec k n); auto with coc ecoc core arith sets; intro a0. elim a0; intros; auto with coc ecoc core arith sets. unfold lift in |- *; auto with ecoc. Qed.
imports: Termes Conv