proposition: Lemma checks_arrow Γ t A B : Γ |-- t <= A ---> B → ∃ t', t = λ t' ∧ A :: Γ |-- t' <= B.
proof: Proof. intros H; inversion H; subst. exists t0; term. inversion H0. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid