lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
lapply (frees_mono … Hz1 … Hf1) -Hz1 #H1
lapply (sor_eq_repl_back1 … Hz … H02) -g0 #Hz
lapply (sor_eq_repl_back2 … Hz … H1) -z1 #Hz
lapply (sor_mono … f Hz ?) // -Hz #H
lapply (sor_inv_sle_sn … Hf) -Hf #Hf
lapply (frees_eq_repl_back … Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
lapply (sor_mono … f Hz ?) // -Hz #H
lapply (sor_inv_sle_sn … Hf) -Hf #Hf
lapply (frees_eq_repl_back … Hf0 (⫯f) ?) /2 width=5 by eq_next/ -z #Hf0
lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
@(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)
lapply (sor_eq_repl_back1 … Hg2 … H0) -z0 #Hg2
lapply (sor_eq_repl_back2 … Hg2 … H1) -z1 #Hg2
@(ex3_2_intro … Hf1 Hf0) -Hf1 -Hf0 (**) (* constructor needed *)