Step
*
of Lemma
sublist_append1
∀[T:Type]. ∀L1,L2:T List. L1 ⊆ L1 @ L2
BY
{ (Auto THEN With ⌜λx.x⌝ (D 0)⋅ THEN Reduce 0 THEN Auto' THEN Try ((D 0 THEN Reduce 0 THEN Auto')⋅)) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}L1,L2:T List. L1 \msubseteq{} L1 @ L2
By
Latex:
(Auto THEN With \mkleeneopen{}\mlambda{}x.x\mkleeneclose{} (D 0)\mcdot{} THEN Reduce 0 THEN Auto' THEN Try ((D 0 THEN Reduce 0 THEN Auto')\mcdot{}))
Home
Index