proposition: Theorem thinning : forall e t T, typ e t T -> forall A, wf (A :: e) -> typ (A :: e) (lift 1 t) (lift 1 T).
proof: Proof. unfold lift in |- *. intros. inversion_clear H0. apply typ_weak_weak with A e; auto with coc core arith datatypes. apply wf_var with s; auto with coc core arith datatypes. Qed.
imports: Termes Conv MyList