dfsb-dval
Theorem.
Arguments:
(st),
(sv),
(pr),
Distinct variable conditions:
(
,
),
Assertions:
([
/
]
((
)
))
Proof:
Hyp
Ref
Line
Expr
dfsb-dvex
1
([
/
]
((
)
))
eqs4lem
2
(
((
)
)
((
)
))
eqs5lem
3
(
((
)
)
((
)
))
2, 3
>bii
4
(
((
)
)
((
)
))
1, 4
bitr
5
([
/
]
((
)
))
(st), 
(sv), 
(pr), (st), (sv), (pr), , ), /]
((
)
))/]
(()
))(())(()))(())(()))(())(()))/](()))