theorem ifr_lift_bi (f) (p) (q) (t1) (t2):
t1 ā”š¢š[p,q] t2 ā ā[f]t1 ā”š¢š[ā[f]p,ā[ā[pāšāš]f]q] ā[f]t2.
#f #p #q #t1 #t2
theorem ifr_lift_bi (f) (p) (q) (t1) (t2):
t1 ā”š¢š[p,q] t2 ā ā[f]t1 ā”š¢š[ā[f]p,ā[ā[pāšāš]f]q] ā[f]t2.
#f #p #q #t1 #t2