diff --git a/src/SExpFunc.res b/src/SExpFunc.res
index 86fa858..6672150 100644
--- a/src/SExpFunc.res
+++ b/src/SExpFunc.res
@@ -144,9 +144,17 @@ module Make = (Atom: ATOM): {
       unifyTerm(x, y)->Seq.flatMap(s1 =>
         a
         ->Array.sliceToEnd(~start=1)
-        ->Array.map(((t1, t2)) => (substitute(t1, s1), substitute(t2, s1)))
+        ->Array.filterMap(((t1, t2)) =>
+          try {Some((substitute(t1, s1), substitute(t2, s1)))} catch {
+          | SubstNotCompatible(_) => None
+          }
+        )
         ->unifyArray
-        ->Seq.map(s2 => combineSubst(s1, s2))
+        ->Seq.filterMap(s2 =>
+          try {Some(combineSubst(s1, s2))} catch {
+          | SubstNotCompatible(_) => None
+          }
+        )
       )
     }
   }
diff --git a/src/Theorem.res b/src/Theorem.res
index 950f3c2..12d3074 100644
--- a/src/Theorem.res
+++ b/src/Theorem.res
@@ -14,7 +14,13 @@ module Make = (
   open RuleView
   module RuleView = RuleView.Make(Term, Judgment, JudgmentView)
   module Ports = Ports(Term, Judgment)
-  type state = {name: string, rule: Rule.t, proof: Proof.t, gen: Term.gen}
+  type state = {
+    name: string,
+    rule: Rule.t,
+    proof: Proof.t,
+    gen: Term.gen,
+    substFailed: option<string>,
+  }
   type props = {
     content: state,
     imports: Ports.t,
@@ -39,7 +45,7 @@ module Make = (
         Error("Trailing input: "->String.concat(s'))
       | Ok((proof, _)) =>
         Ok((
-          {name, rule, proof, gen},
+          {name, rule, proof, gen, substFailed: None},
           {Ports.facts: Dict.fromArray([(name, rule)]), ruleStyle: None},
         ))
       }
@@ -51,15 +57,21 @@ module Make = (
     let checked = Proof.check(ctx, props.content.proof, props.content.rule)
     let sidebarRef = React.useRef(Nullable.null)
     let proofChanged = (proof, subst) => {
+      let proof = Proof.uncheck(proof)->Proof.substitute(subst)
       props.onChange(
-        {...props.content, proof: Proof.uncheck(proof)->Proof.substitute(subst)},
+        try {
+          Proof.check(ctx, proof, props.content.rule)->ignore
+          {...props.content, proof, substFailed: None}
+        } catch {
+        | SExpFunc.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)}
+        },
         ~exports={
           Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]),
           ruleStyle: None,
         },
       )
     }
-    
+
     <SidebarContext sidebarRef>
       <h3> {React.string("Theorem")} </h3>
       <RuleView rule={props.content.rule} scope={[]} style={ruleStyle}>
@@ -69,6 +81,10 @@ module Make = (
       <ProofView
         ruleStyle={ruleStyle} scope={[]} proof=checked gen={props.content.gen} onChange=proofChanged
       />
+      {switch props.content.substFailed {
+      | Some(msg) => React.string(msg)
+      | None => React.null
+      }}
       <div className="sidebar" ref={ReactDOM.Ref.domRef(sidebarRef)} />
     </SidebarContext>
   }