lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
t1 Ļµ š ā t1ā(pāš¦) Ļµ š ā
t1 ā”š¢š[p,q] t2 ā ā¼[f]t1 ā”š¢š[āp,āq] ā¼[f]t2.
#f #p #q #t1 #t2 #H1t1 #H2t1
lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
t1 Ļµ š ā t1ā(pāš¦) Ļµ š ā
t1 ā”š¢š[p,q] t2 ā ā¼[f]t1 ā”š¢š[āp,āq] ā¼[f]t2.
#f #p #q #t1 #t2 #H1t1 #H2t1