At: normalization lemma 1 1 1 1 1 1 1 4 1 1 1
1. hyp: Formula List
2. concl: Formula List
3. 
f
hyp.(
(f) > 0)
4. M: Formula List
5. N: Formula List
6. f: Formula
7. x1: Formula
8. x2: Formula
9. (x1
x2) > 0
10. hyp = (M @ (x1x2.N))
11. ( < x2.(M @ N),concl > ) < ( < M @ (x1x2.N),concl > ) 
(L:Sequent List.
sL.((s) = 0)
& (sL.|= s |= < x2.(M @ N),concl > )
& (a:Assignment. sL.a |
s a | < x2.(M @ N),concl > ))
( < x1.(M @ N),concl > ) < ( < M @ (x1x2.N),concl > )
By:
SequentRankReduce 0
THEN
GenConclOnAps
Generated subgoals:None
About:
