(* Constructions with lift **************************************************)
theorem ifr_lift_bi (f) (t1) (t2) (r):
(* Constructions with lift **************************************************)
theorem ifr_lift_bi (f) (t1) (t2) (r):
(* Note: crux of the proof begins *)
@(stream_eq_trans โฆ (tr_compose_uni_dx_pap โฆ)) <tr_pap_succ_nap
@tr_compose_eq_repl // >nsucc_unfold
(* Note: crux of the proof begins *)
@(stream_eq_trans โฆ (tr_compose_uni_dx_pap โฆ)) <tr_pap_succ_nap
@tr_compose_eq_repl // >nsucc_unfold