proposition: Lemma check_types : (forall Γ t T, Γ |-- t <= T -> Γ |-- t : T) with synthetizes_types : (forall Γ t T, Γ |-- t => T -> Γ |-- t : T).
proof: Proof. intros. destruct H; try econstructor; term. intros. destruct H; try solve [ econstructor; term ]. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid