iDestruct on non-existing name yields "no matching clause for match"
Title says it all. Goal state:
============================
"Hincl" : type_incl ty1 ty2
"Hsz" : ⌜ty_size ty1 = ty_size ty2⌝
"Hoincl" : ∀ (tid0 : thread_id) (vl : list val), ty_own ty1 tid0 vl -∗ ty_own ty2 tid0 vl
"Hsincl" : ∀ (κ0 : lft) (tid0 : thread_id) (l0 : loc),
ty_shr ty1 κ0 tid0 l0 -∗ ty_shr ty2 κ0 tid0 l0
--------------------------------------□
"Hshr" : ty_shr (rc ty1) κ tid l
--------------------------------------∗
ty_shr (rc ty2) κ tid l
Tactic: iDestruct "Hst" as (??) "H".
Error: Error: No matching clauses for match.