proposition: Lemma ct_ind_left_helper P (G: good_ctx P) x r (EQ: x = r⁺) r' : P r ⊆ r' -> (forall k, P k ⊆ r' -> P (r ⨾ k) ⊆ r') -> P x ⊆ r'.
proof: Proof. by subst; apply ct_ind_left. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets