Step * 1 1 1 of Lemma assert_of_bpermr


1. DSet
2. |s|
3. |s| List
4. [] ≡(|s|) [u v]
⊢ False
BY
TACTIC:((InvertRel (-1) THENM (MoveToConcl (-1) THEN Fold `not` 0)) THENA Auto) }

1
1. DSet
2. |s|
3. |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