proposition: Theorem substitution : forall e t u (U : term), typ (t :: e) u U -> forall d : term, typ e d t -> typ e (subst d u) (subst d U).
proof: Proof. intros. unfold subst in |- *. apply typ_sub_weak with e t (t :: e); auto with coc core arith datatypes. apply typ_wf with d t; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList