proposition: Lemma check_normal {Γ t T} : Γ |-- t <= T -> normal t with synth_neutral {Γ t T} : Γ |-- t => T -> neutral t.
proof: Proof. destruct 1; constructor; term. destruct 1; constructor; term. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia Relations Setoid