proposition: Lemma ct_ind_right P (G: good_ctx P) r r' : P r ⊆ r' -> (forall k, P k ⊆ r' -> P (k ⨾ r) ⊆ r') -> P ( r⁺ ) ⊆ r'.
proof: Proof. ins; cdes G; rewrite (proj1 (ctEE _)). etransitivity; [eapply CUN|apply inclusion_bunion_l]; ins. induction x; ins; eauto. by rewrite (proj1 (seq_id_l _)). Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets