#S #e1 #i
cut (e1 ⊙ 〈i,true〉 = 〈fst \dots (e1 ▹ i), snd \dots(e1 ▹ i) ∨ true〉) [//]
#H >H cases (e1 ▹ i) #i1 #b1 cases b1
[>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
#S #e1 #i
cut (e1 ⊙ 〈i,true〉 = 〈fst \dots (e1 ▹ i), snd \dots(e1 ▹ i) ∨ true〉) [//]
#H >H cases (e1 ▹ i) #i1 #b1 cases b1
[>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]