Abduction: More SeLFiE assertions to prune bad conjectures.

[yutakang]

• the flipped final goal as a sub-term.
  • qrevflat var_0 nil2 = revflat var_0 ⟹ qrevflat var_0 (rev var_1) = x (revflat var_0) (rev var_1)
• nested equality
  • (qrevflat var_0 nil2 = revflat var_0) = (qrevflat var_0 (x (rev var_1) nil2) = x (revflat var_0) (rev var_1))
• a compound term appears twice and a variable only appears within this compound term.
  • x (qrevflat var_0 nil2) (rev var_1) = qrevflat var_0 (rev var_1)
• equality over function application whose arguments are the same except for one.
  • x (qrevflat var_0 nil2) nil2 = x (revflat var_0) nil2 ⟹ x (qrevflat var_0 (x (rev var_1) nil2)) nil2 = x (x (revflat var_0) (rev var_1)) nil2
• a variable (var_3) appears only once as an argument to an equality.
  • (⋀a. qrevflat var_0 a = x (revflat var_0) a) ⟹ x (revflat var_0) (x (rev var_1) var_2) = var_3