proposition: Lemma rt_ind_left P (G: good_ctx P) r r' : P ⦗fun _ => True⦘ ⊆ r' -> (forall k, P k ⊆ r' -> P (r ⨾ k) ⊆ r') -> P r＊ ⊆ r'.
proof: Proof. ins; cdes G; rewrite (proj1 (rtEE _)). etransitivity; [eapply CUN|apply inclusion_bunion_l]; ins. induction x; ins; rewrite (proj1 (seq_pow_l _ _)); eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets