proposition: Lemma Etyp_free_db : forall (e : env) (t T : term), Etyp e t T -> free_db (length e) t.
proof: Proof. simple induction 1; intros; auto with coc ecoc core arith datatypes. inversion_clear H1. apply db_ref. elim H3; simpl in |- *; intros; auto with coc ecoc core arith datatypes. Qed.
imports: Termes Conv Ered MyList Types