Bad error message for failing iInduction
I am not sure what is going wrong with the following iInduction
, and IPM's error doesn't tell me:
Inductive val :=
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val).
Lemma test {Σ} (val_rel : val → val → iProp Σ) v_t v_s :
val_rel v_t v_s -∗ True.
Proof. iInduction v_t as [| |] "IH" forall v_s.
(* Error: No matching clauses for match. *)