proposition: Lemma type_assignmentE Gamma M t : type_assignment Gamma M t -> match M with | var x => type_assignment_var_spec Gamma x t | lam M' => match t with | atom _ => False | arr s' phi' t' => type_assignment ((s', phi') :: Gamma) M' t' end | app M' N' => type_assignment_app_spec Gamma M' N' t end.
proof: Proof. by case=> * //; econstructor; eassumption. Qed.
imports: Undecidability.IntersectionTypes.CD PeanoNat List Relations Lia Undecidability.LambdaCalculus.Lambda Undecidability.LambdaCalculus.Util.term_facts ssreflect