proposition: Lemma ct_lift : (rel_lift eqv r)⁺ ≡ rel_lift eqv (r ⨾ eqv)⁺.
proof: Proof. Proof using REFL SYM TRAN. split; red; ins. { u; induction H; desf; eauto. { do 2 eexists; splits; eauto 6 using t_step. } exists x1, y0; splits; try eapply t_trans with x0; eauto. apply ct_end in IHclos_trans1; u. apply ct_end; u; do 2 (eexists; split; eauto). } red in H; desf; generalize dependent x; generalize dependent y. apply clos_trans_t1n in H. induction H; ins; desf; red in H; desc. apply t_step; u; do 2 eexists; splits; eauto. eapply t_trans; eauto. eapply t_step; u; do 2 eexists; splits; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic Setoid HahnEquational