proposition: Lemma Forall_all {X : Type} {P : X -> Prop} l : Forall P l <-> all P l.
proof: Proof. elim: l. { done. } move=> ?? IH. split. - by move=> /Forall_cons_iff [? /IH]. - move=> [? ?]. constructor; first done. by apply /IH. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect