proposition: Fact imsell_tps_lbang m Γ : m ≼ Γ -> ⟪‼Γ⟫ ⊆ K m.
proof: Proof. Proof using HK_unit0 HK_plus HK_antitone. induction Γ as [ | (v,A) Γ IH ]; simpl; intros H1 x. + intros <-; auto. + intros (y & z & -> & (G1 & G2) & G3). apply HK_plus; exists y, z; msplit 2; auto. * revert G2; apply HK_antitone; auto. apply (H1 (v,A)); auto. * revert G3; apply IH. intros (w,B) ?; apply (H1 (_,B)); auto. Qed.
imports: List Permutation Undecidability.ILL(IMSELL) Undecidability.Shared.Libs.DLW(utils pos vec)