Nuprl - Pf zero_rank_all_vars 1 2 1 1 1 1

PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

1. L: Sequent List
2. eqS: {Sequent=}
3. eqF: {Formula=}
4. sL.((s) = 0)
5. hyp: Formula List
6. concl: Formula List
7. < hyp,concl > (eqS) L
8. z: Formula
9. z(eqF) concl
10. M: Formula List
11. N: Formula List
12. concl = (M @ (z.N))
13. (hyp)+(M @ (z.N)) = 0

v:Var. z = v

By: Rewrite (HigherC list_rank_append_conv) -1 THEN AbReduce -1

Generated subgoal:

1 13. (hyp)+(M)+(z)+(N) = 0
v:Var. z = v

About: