Lemma correctness : (forall (gamma : environment) (t : term) (tt : type),
             has_type gamma t tt -> (type_check gamma t) = Some({ tt | has_type gamma t tt})).