/3 width=7 by sor_pp, sor_np/
qed.
+lemma sor_isid: âf1,f2,f. đâŚf1⌠â đâŚf2⌠â đâŚf⌠â f1 â f2 ⥠f.
+/4 width=3 by sor_eq_repl_back2, sor_eq_repl_back1, isid_inv_eq_repl/ qed.
+
(* Inversion lemmas on test for identity ************************************)
lemma sor_isid_inv_sn: âf1,f2,f. f1 â f2 ⥠f â đâŚf1⌠â f2 â f.