proposition: Lemma G_cons Gamma A s gamma: G Gamma gamma -> E A s -> G (A :: Gamma) (s .: gamma).
proof: Proof. intros. intros [|] B H'; cbn in *. now injection H' as ->. now eapply H. Qed.
imports: Morphisms Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence typing order)