make substitution part of lang interface and use that for fn calls

_CoqProject

theories/simplang/behavior.v

theories/simplang/gen_adequacy.v

theories/simplang/gen_log_rel.v

theories/simplang/gen_refl.v

theories/simplang/gen_val_rel.v

theories/simplang/globalbij.v

theories/simplang/lang.v

theories/simplang/na_inv/adequacy.v

theories/simplang/na_inv/examples/data_races.v

theories/simplang/na_inv/examples/remove_alloc.v

theories/simplang/na_inv/readonly_refl.v

theories/simplang/na_inv/refl.v

theories/simplang/parallel_subst.v

theories/simplang/primitive_laws.v

theories/simplang/proofmode.v

theories/simplang/pure_refl.v

theories/simplang/simple_inv/adequacy.v

theories/simplang/simple_inv/refl.v

theories/simplang/tactics.v