(* Main inversions **********************************************************)
(*** after_inv_total *)
-lemma pr_after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89¡ f.
+lemma pr_after_inv_total: â\88\80f2,f1,f. f2 â\8a\9a f1 â\89\98 f â\86\92 f2 â\88\98 f1 â\89\90 f.
/2 width=4 by pr_after_mono/ qed-.