ā[f](t[āpāu]) ā (ā[f]t)[ā(āp)āā[ā[p]f]u].
#f #t #u #p #Hu #H1p #H2p #ql * #q * *
[ #r #Hu #H1 #H2 destruct
@or_introl @ex2_intro
ā[f](t[āpāu]) ā (ā[f]t)[ā(āp)āā[ā[p]f]u].
#f #t #u #p #Hu #H1p #H2p #ql * #q * *
[ #r #Hu #H1 #H2 destruct
@or_introl @ex2_intro