diff options
Diffstat (limited to 'src/Util/WordUtil.v')
-rw-r--r-- | src/Util/WordUtil.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 6a8831b14..9e88c1731 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -59,3 +59,7 @@ Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with | eq_refl => w end)); abstract omega. Defined. + +Lemma combine_eq_iff {a b} (A:word a) (B:word b) C : + combine A B = C <-> A = split1 a b C /\ B = split2 a b C. +Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed. |