#f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
#Hf2 #Hf1 #H2 @pr_isi_pat_total // -Hf1
#i1 #i2 #Hi12 elim (pr_after_des_ist_pat … Hi12 … Hf) -f1
#f2 #f1 #f #H #Hf elim (pr_after_inv_ist … Hf H) -H
#Hf2 #Hf1 #H2 @pr_isi_pat_total // -Hf1
#i1 #i2 #Hi12 elim (pr_after_des_ist_pat … Hi12 … Hf) -f1