Add SmartPairf_Pair

1 files changed, 3 insertions, 0 deletions

diff --git a/src/Reflection/SmartMap.v b/src/Reflection/SmartMap.v
index f6619f449..d38b5c733 100644
--- a/src/Reflection/SmartMap.v
+++ b/src/Reflection/SmartMap.v
@@ -110,6 +110,9 @@ Section homogenous_type.
       and not just [base_type_code] *)
   Definition SmartPairf {t} : interp_flat_type exprf t -> exprf t
     := @smart_interp_flat_map exprf exprf (fun t x => x) TT (fun A B x y => Pair x y) t.
+  Lemma SmartPairf_Pair {A B} e1 e2
+    : SmartPairf (t:=Prod A B) (e1, e2)%core = Pair (SmartPairf e1) (SmartPairf e2).
+  Proof. reflexivity. Qed.
   Definition SmartVarf {t} : interp_flat_type var t -> exprf t
     := @smart_interp_flat_map var exprf (fun t => Var) TT (fun A B x y => Pair x y) t.
   Definition SmartVarfMap {var var'} (f : forall t, var t -> var' t) {t}