Step * of Lemma l_contains_append2

[T:Type]. ∀A,B:T List.  A ⊆ A
BY
(Intros
   THEN Unfold `l_contains` 0
   THEN (RWO "l_all_iff" THENA Auto)
   THEN RWO "member_append" 0
   THEN Auto
   THEN OrRight
   THEN Auto) }


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}A,B:T  List.    A  \msubseteq{}  B  @  A


By


Latex:
(Intros
  THEN  Unfold  `l\_contains`  0
  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
  THEN  RWO  "member\_append"  0
  THEN  Auto
  THEN  OrRight
  THEN  Auto)




Home Index