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.
cc @jung