Step
*
1
1
1
of Lemma
assert_of_bpermr
1. s : DSet
2. u : |s|
3. v : |s| List
4. [] ≡(|s|) [u / v]
⊢ False
BY
{ TACTIC:((InvertRel (-1) THENM (MoveToConcl (-1) THEN Fold `not` 0)) THENA Auto) }
1
1. s : DSet
2. u : |s|
3. v : |s| List
⊢ ¬([u / v] ≡(|s|) [])
Latex:
Latex:
1.  s  :  DSet
2.  u  :  |s|
3.  v  :  |s|  List
4.  []  \mequiv{}(|s|)  [u  /  v]
\mvdash{}  False
By
Latex:
TACTIC:((InvertRel  (-1)  THENM  (MoveToConcl  (-1)  THEN  Fold  `not`  0))  THENA  Auto)
Home
Index