Step
*
of Lemma
l_disjoint_cons
∀[T:Type]. ∀[a,b:T List]. ∀[x:T]. uiff(l_disjoint(T;a;[x / b]);(¬(x ∈ a)) ∧ l_disjoint(T;a;b))
BY
{ ((UnivCD THENA Auto)
THEN (Subst ⌜[x / b] ~ [x] @ b⌝ 0⋅ THENA (Reduce 0 THEN Auto))
THEN (RWO "l_disjoint_append" 0 THENA Auto)
THEN (RWO "l_disjoint_singleton" 0 THENA Auto)
THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[a,b:T List]. \mforall{}[x:T]. uiff(l\_disjoint(T;a;[x / b]);(\mneg{}(x \mmember{} a)) \mwedge{} l\_disjoint(T;a;b))
By
Latex:
((UnivCD THENA Auto)
THEN (Subst \mkleeneopen{}[x / b] \msim{} [x] @ b\mkleeneclose{} 0\mcdot{} THENA (Reduce 0 THEN Auto))
THEN (RWO "l\_disjoint\_append" 0 THENA Auto)
THEN (RWO "l\_disjoint\_singleton" 0 THENA Auto)
THEN Auto)
Home
Index