proposition: Lemma ct_ind_left P (G: good_ctx P) r r' : P r ⊆ r' -> (forall k, P k ⊆ r' -> P (r ⨾ k) ⊆ r') -> P ( r⁺ ) ⊆ r'.
proof: Proof. ins; cdes G; rewrite (proj1 (ct_end _)). apply rt_ind_left with (P := fun x => P (x ⨾ r)); ins; eauto using good_ctx_compose, good_ctx_seq_l, good_ctx_id. by rewrite (proj1 (seq_id_l _)). by rewrite (proj1 (seqA _ _ _)); eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets