-| #u #n #Hu * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
-| #u #Hu * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
-| #v #u #Hv #Hu * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
+| #u #n #Hu #_ * #q #Hq #Hp /3 width=7 by ex4_3_intro, or5_intro1/
+| #u #Hu #_ * #q #Hq #Hp /3 width=6 by or5_intro2, ex4_2_intro/
+| #v #u #Hv #Hu #_ #_ * * #q #Hq #Hp /3 width=8 by ex5_3_intro, or5_intro3, or5_intro4/
+| #t1 #t2 #Ht12 #_ #IH #Ht2
+ elim IH -IH [6: /2 width=3 by subset_in_eq_repl_fwd/ ] *
+ [ /4 width=3 by subset_eq_trans, or5_intro0, ex2_intro/
+ | /4 width=7 by subset_eq_trans, ex4_3_intro, or5_intro1/
+ | /4 width=6 by subset_eq_trans, or5_intro2, ex4_2_intro/
+ | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro3/
+ | /4 width=8 by subset_eq_trans, ex5_3_intro, or5_intro4/
+ ]