proposition: Theorem cancelR j k t1 t2 h1 h2 (f1 : Ast empc j t1 h1) (f2 : Ast j k t2 h2) : def h1 -> h1 = h2 -> eval k (cancel k t1 t2).
proof: Proof. case: f1 f2=>[[<- _ I]] [[<- S _]] D H. by apply: cancel_sound; rewrite -(interp_subctx I S). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat seq eqtype) LemmaOverloading(prelude heaps terms prefix xfindCTC)