Theorem: Smt.Reconstruct.Prop.orN_append_right (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
qs ps : List Prop
hqs : orN qs
⊢ orN (ps ++ qs)
Tactic:
apply @orN_subList qs (ps ++ qs) ps.length (ps.length + qs.length) hqs
State after:
qs ps : List Prop
hqs : orN qs
⊢ qs = subList' (ps ++ qs) ps.length (ps.length + qs.length)

State before:
qs ps : List Prop
hqs : orN qs
⊢ qs = subList' (ps ++ qs) ps.length (ps.length + qs.length)
Tactic:
simp only [←length_append, subList', take_length, drop_append]
State after:
no goals