fact: Definition inst_exec_eff (l: N.ICExec.Label): InstSyntax.ExtLabel := match l with | N.ICExec.put_label no n c k v s s' u => ext_put_label _ n k (InstSyntaxArg.inst_val n c v) | N.ICExec.get_label no n' c' n k s s' v => ext_get_label _ n k (InstSyntaxArg.inst_val n' c' v) | N.ICExec.update_label no n' c' n k v s m s' => ext_put_label _ n k (InstSyntaxArg.inst_val n' c' v) | N.ICExec.fault_label no n s s' => ext_fault_label _ n end.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)