diff --git a/cranelift/codegen/src/isa/aarch64/lower/isle.rs b/cranelift/codegen/src/isa/aarch64/lower/isle.rs
index 0c3f151c4818..6e752496c093 100644
--- a/cranelift/codegen/src/isa/aarch64/lower/isle.rs
+++ b/cranelift/codegen/src/isa/aarch64/lower/isle.rs
@@ -22,8 +22,8 @@ use crate::machinst::{isle::*, InputSourceInst};
 use crate::{
     binemit::CodeOffset,
     ir::{
-        immediates::*, types::*, AtomicRmwOp, BlockCall, ExternalName, Inst, InstructionData,
-        MemFlags, TrapCode, Value, ValueList,
+        immediates::*, types::*, ArgumentExtension, AtomicRmwOp, BlockCall, ExternalName, Inst,
+        InstructionData, MemFlags, TrapCode, Value, ValueList,
     },
     isa::aarch64::abi::AArch64CallSite,
     isa::aarch64::inst::args::{ShiftOp, ShiftOpShiftImm},
diff --git a/cranelift/isle/isle/isle_examples/pass/veri_spec.isle b/cranelift/isle/isle/isle_examples/pass/veri_spec.isle
index 886f1ffcf81d..273b6132c4b1 100644
--- a/cranelift/isle/isle/isle_examples/pass/veri_spec.isle
+++ b/cranelift/isle/isle/isle_examples/pass/veri_spec.isle
@@ -8,7 +8,7 @@
   ((args (bv 64)) (ret (bv 64)) (canon (bv 64)))
 )
 
-(spec (A i j) (provide (= (if true (= i j) (= i (bvneg j))))))
+(spec (A i j) (provide (= (if true (= i j) (= i (bvneg j))) (=> false true))))
 (instantiate A ((args (bv 8)) (ret (bv 8)) (canon (bv 8))))
 (decl A (u8 u8) u8)
 
diff --git a/cranelift/isle/isle/src/ast.rs b/cranelift/isle/isle/src/ast.rs
index 5aefba303add..a3fb0ef72c50 100644
--- a/cranelift/isle/isle/src/ast.rs
+++ b/cranelift/isle/isle/src/ast.rs
@@ -141,6 +141,7 @@ pub enum SpecOp {
     And,
     Or,
     Not,
+    Imp,
 
     // Integer comparisons
     Lt,
diff --git a/cranelift/isle/isle/src/parser.rs b/cranelift/isle/isle/src/parser.rs
index c219e705ab91..9af80f6dd539 100644
--- a/cranelift/isle/isle/src/parser.rs
+++ b/cranelift/isle/isle/src/parser.rs
@@ -474,6 +474,7 @@ impl<'a> Parser<'a> {
             "=" => Ok(SpecOp::Eq),
             "and" => Ok(SpecOp::And),
             "not" => Ok(SpecOp::Not),
+            "=>" => Ok(SpecOp::Imp),
             "or" => Ok(SpecOp::Or),
             "<=" => Ok(SpecOp::Lte),
             "<" => Ok(SpecOp::Lt),
diff --git a/cranelift/isle/isle/src/printer.rs b/cranelift/isle/isle/src/printer.rs
index 1cd8e372d247..a7ed0475c73c 100644
--- a/cranelift/isle/isle/src/printer.rs
+++ b/cranelift/isle/isle/src/printer.rs
@@ -228,6 +228,7 @@ impl Printable for SpecOp {
             SpecOp::Eq => "=",
             SpecOp::And => "and",
             SpecOp::Not => "not",
+            SpecOp::Imp => "=>",
             SpecOp::Or => "or",
             SpecOp::Lte => "<=",
             SpecOp::Lt => "<",
diff --git a/cranelift/isle/veri/veri_engine/src/annotations.rs b/cranelift/isle/veri/veri_engine/src/annotations.rs
index 4e4dafef2988..c796dc1d7a7d 100644
--- a/cranelift/isle/veri/veri_engine/src/annotations.rs
+++ b/cranelift/isle/veri/veri_engine/src/annotations.rs
@@ -141,6 +141,7 @@ fn spec_op_to_expr(s: &SpecOp, args: &Vec<SpecExpr>, pos: &Pos, env: &ParsingEnv
         SpecOp::Lte => binop(|x, y| Expr::Lte(x, y), args, pos, env),
         SpecOp::Gt => binop(|x, y| Expr::Lt(y, x), args, pos, env),
         SpecOp::Gte => binop(|x, y| Expr::Lte(y, x), args, pos, env),
+        SpecOp::Imp => binop(|x, y| Expr::Imp(x, y), args, pos, env),
         SpecOp::BVAnd => binop(|x, y| Expr::BVAnd(x, y), args, pos, env),
         SpecOp::BVOr => binop(|x, y| Expr::BVOr(x, y), args, pos, env),
         SpecOp::BVXor => binop(|x, y| Expr::BVXor(x, y), args, pos, env),
diff --git a/cranelift/isle/veri/veri_engine/src/type_inference.rs b/cranelift/isle/veri/veri_engine/src/type_inference.rs
index 67dfad805fcf..43c1942c83a2 100644
--- a/cranelift/isle/veri/veri_engine/src/type_inference.rs
+++ b/cranelift/isle/veri/veri_engine/src/type_inference.rs
@@ -446,6 +446,24 @@ fn add_annotation_constraints(
                 t,
             )
         }
+        annotation_ir::Expr::Imp(x, y) => {
+            let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
+            let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
+            let t = tree.next_type_var;
+
+            tree.concrete_constraints
+                .insert(TypeExpr::Concrete(t1, annotation_ir::Type::Bool));
+            tree.concrete_constraints
+                .insert(TypeExpr::Concrete(t2, annotation_ir::Type::Bool));
+            tree.concrete_constraints
+                .insert(TypeExpr::Concrete(t, annotation_ir::Type::Bool));
+
+            tree.next_type_var += 1;
+            (
+                veri_ir::Expr::Binary(veri_ir::BinaryOp::Imp, Box::new(e1), Box::new(e2)),
+                t,
+            )
+        }
         annotation_ir::Expr::Lte(x, y) => {
             let (e1, t1) = add_annotation_constraints(*x, tree, annotation_info);
             let (e2, t2) = add_annotation_constraints(*y, tree, annotation_info);
@@ -1358,8 +1376,6 @@ fn add_annotation_constraints(
             tree.next_type_var += 1;
             (veri_ir::Expr::BVPopcnt(Box::new(e1)), t)
         }
-
-        _ => todo!("expr {:#?} not yet implemented", expr),
     };
     tree.ty_vars.insert(e.clone(), t);
     // let fmt = format!("{}:\t{:?}", t, e);