Prove Gremlin is semantically untyped

_CoqProject

theories/logrel/F_mu_ref_conc_gremlin_sem_untyped/base.v

..._ref_conc_gremlin_sem_untyped/binary/context_refinement.v

...mu_ref_conc_gremlin_sem_untyped/binary/examples/counter.v

.../F_mu_ref_conc_gremlin_sem_untyped/binary/examples/fact.v

.../F_mu_ref_conc_gremlin_sem_untyped/binary/examples/lock.v

...conc_gremlin_sem_untyped/binary/examples/stack/CG_stack.v

...conc_gremlin_sem_untyped/binary/examples/stack/FG_stack.v

...nc_gremlin_sem_untyped/binary/examples/stack/refinement.v

...c_gremlin_sem_untyped/binary/examples/stack/stack_rules.v

...el/F_mu_ref_conc_gremlin_sem_untyped/binary/fundamental.v

.../logrel/F_mu_ref_conc_gremlin_sem_untyped/binary/logrel.v

...s/logrel/F_mu_ref_conc_gremlin_sem_untyped/binary/rules.v

...grel/F_mu_ref_conc_gremlin_sem_untyped/binary/soundness.v

theories/logrel/F_mu_ref_conc_gremlin_sem_untyped/lang.v

theories/logrel/F_mu_ref_conc_gremlin_sem_untyped/typing.v

..._ref_conc_gremlin_sem_untyped/unary/examples/symbol_nat.v

...rel/F_mu_ref_conc_gremlin_sem_untyped/unary/fundamental.v

...s/logrel/F_mu_ref_conc_gremlin_sem_untyped/unary/logrel.v

...ogrel/F_mu_ref_conc_gremlin_sem_untyped/unary/soundness.v