Step
*
of Lemma
iseg_antisymmetry
∀[T:Type]. ∀[as,bs:T List]. (as = bs ∈ (T List)) supposing (bs ≤ as and as ≤ bs)
BY
{ xxx(((((InductionOnList THEN InductionOnList THEN Auto THEN (All (RWO "iseg_nil"))) THENM All Reduce)
THEN Auto
THEN (All (RWO "cons_iseg")))
THENM All Reduce
)
THEN Auto
THEN EqCD
THEN Auto
THEN BackThruSomeHyp
THEN Auto)xxx }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[as,bs:T List]. (as = bs) supposing (bs \mleq{} as and as \mleq{} bs)
By
Latex:
xxx(((((InductionOnList THEN InductionOnList THEN Auto THEN (All (RWO "iseg\_nil")))
THENM All Reduce
)
THEN Auto
THEN (All (RWO "cons\_iseg")))
THENM All Reduce
)
THEN Auto
THEN EqCD
THEN Auto
THEN BackThruSomeHyp
THEN Auto)xxx
Home
Index