Commit 8d08daca authored by Dan Frumin's avatar Dan Frumin

Better `unfold` rule for the `typeable` database.

parent 8d103530
......@@ -105,6 +105,15 @@ Proof. intros. subst τ. by econstructor. Qed.
Hint Resolve BINOP' : typeable.
Remove Hints BinOp_typed : typeable.
Lemma TUNFOLD' Γ e τ τ' :
Γ ⊢ₜ e : TRec τ
τ' = τ.[TRec τ/]
Γ ⊢ₜ Unfold e : τ'.
Proof. intros. subst τ'. by econstructor. Qed.
Hint Resolve TUNFOLD' : typeable.
Remove Hints TUnfold : typeable.
Hint Constructors EqType : typeable.
Hint Extern 10 (<[_:=_]>_ !! _ = Some _) => eapply lookup_insert : typeable.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment