------------------------------- MODULE Dummy -------------------------------
EXTENDS TLAPS
CONSTANT Elems
ASSUME \E x : x \in Elems

Insert[new \in Elems, set \in SUBSET Elems] ==
  set \cup {new} 

InsertOp(new, set) ==
  set \cup {new}

THEOREM \A x \in Elems, set \in SUBSET Elems: 
  x \in Insert[x, set]
  <1> SUFFICES ASSUME NEW x \in Elems, NEW set \in SUBSET Elems
               PROVE  x \in Insert[x, set]
    OBVIOUS
  <1> QED
    BY DEF Insert

THEOREM \A x \in Elems, set \in SUBSET Elems:
  x \in InsertOp(x, set)
  <1>a SUFFICES ASSUME NEW x \in Elems, NEW set \in SUBSET Elems
               PROVE  x \in InsertOp(x, set)
    OBVIOUS
  <1>b QED
    BY DEF InsertOp
=============================================================================
\* Modification History
\* Last modified Thu Jun 20 12:30:32 AST 2019 by marko
\* Created Thu Jun 13 13:34:49 AST 2019 by marko