âf2,f1,f. đâȘfâ« â f2 â f1 â f â f2 ⥠f â đâȘf1â«.
#f2 #f1 #f #H #Hf elim (gr_after_inv_ist ⊠Hf H) -H
#Hf2 #Hf1 #H2 @gr_isi_pat_total // -Hf1
âf2,f1,f. đâȘfâ« â f2 â f1 â f â f2 ⥠f â đâȘf1â«.
#f2 #f1 #f #H #Hf elim (gr_after_inv_ist ⊠Hf H) -H
#Hf2 #Hf1 #H2 @gr_isi_pat_total // -Hf1