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

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

State before:
ps qs : List Prop
hps : orN ps
⊢ ps = subList' (ps ++ qs) 0 ps.length
Tactic:
simp [subList', take_append]
State after:
no goals