137 translator simulations, dep_comb_witness1_eq and dep_parse_comparable_data_eq
-
dep_comb_witness1_eq
anddep_parse_comparable_data_eq
are proved. - move 2 lemmas from
Proofs/Script_ir_translator.v
toProofs/Script_typed_ir.v
. - minor code cleanups
Edited by Andrey Klaus