PrintForm
Definitions
assignment
Sections
ClassicalProps(jlc)
Doc
At:
restriction
wf
1
1
1.
a':
Assignment
2.
a:
Assignment
3.
x:
Var
case (a(x)): 3
(a'(x)); 3
3
; 3
(a'(x));
By:
GenConclOnAps
Generated subgoal:
1
4.
n:
5.
a(x) = n
6.
n1:
7.
a'(x) = n1
8.
n2:
9.
a'(x) = n2
case n: 3
n1; 3
3
; 3
n1;
About: