proposition: Lemma delift_ct_lift : rel_delift eqv (rel_lift eqv r)⁺ ≡ eqv ⨾ (r ⨾ eqv)⁺.
proof: Proof. Proof using REFL SYM TRAN. rewrite ct_lift, delift_lift, ct_end, !seqA. do 3 (apply seq_more; ins). u; split; ins; desf; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic Setoid HahnEquational