mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly2 / emulator / opcodes / IP2022_instr_mode.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/IP2022_instr_mode.ma b/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/IP2022_instr_mode.ma
old mode 100755 (executable)
new mode 100644 (file)
index 0029847..68968a1
--- a/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/IP2022_instr_mode.ma
+++ b/helm/software/matita/contribs/ng_assembly2/emulator/opcodes/IP2022_instr_mode.ma
@@ -67,3 +67,19 @@ nlemma symmetric_eqIP2022im : symmetricT IP2022_instr_mode bool eq_IP2022_im.
           napply (neq_to_neqIP2022im n2 n1 (symmetric_neq ? n1 n2 H))
  ##]
 nqed.
+
+nlemma IP2022im_is_comparable : comparable.
+ @ IP2022_instr_mode
+  ##[ napply MODE_INH
+  ##| napply forall_IP2022_im
+  ##| napply eq_IP2022_im
+  ##| napply eqIP2022im_to_eq
+  ##| napply eq_to_eqIP2022im
+  ##| napply neqIP2022im_to_neq
+  ##| napply neq_to_neqIP2022im
+  ##| napply decidable_IP2022im
+  ##| napply symmetric_eqIP2022im
+  ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr IP2022im_is_comparable ≡ IP2022_instr_mode.