iFrame should support conjunction
as in line 235 of
tests/ticket_lock.v, the goal is in form of
H1 /\ H2 /\ ..., and hypothesis are all in the context.
Now what I am doing is
repeat (iSplit; first by auto). The same effect should be achieved by a simple
iFrame as well.