Removes pred_in_dom

hephaestus-pl · May 5, 2017 · b56a8e6 · b56a8e6
1 parent 57ecd0d
commit b56a8e6
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 11 deletions.
diff --git a/src/FFJ/Lemmas.v b/src/FFJ/Lemmas.v
@@ -255,7 +255,7 @@ Proof.
   intros_all. gen Ds D.
   induction H; let X:=fresh "H" in intros Ds D X; induction X; subst; repeat unify_find_refinement; crush.
   destruct H2 with S; crush.
-  unify_pred. lets ?H: H2. apply pred_in_dom in H2; decompose_exs.
+  unify_pred.
   eapply IHmnotin_refinement; eauto.
 Qed.
 

diff --git a/src/FFJ/Semantics.v b/src/FFJ/Semantics.v
@@ -255,15 +255,6 @@ Proof.
   exact RT_wellformed.
 Qed.
 
-
-Lemma pred_in_dom: forall Cl S,
-  pred S Cl ->
-  exists CD, find_refinement S CD.
-Proof.
-  assert (forall R, In R RT -> CRType_OK R). apply Forall_forall.
-  exact RT_wellformed. intros. destruct S. inversion H0. subst.
-Admitted.
-
 Lemma pred_in_dom': forall Cl S,
   pred S Cl ->
   exists CD, find_refinement Cl CD.
@@ -284,7 +275,7 @@ Proof.
   apply filter_In in H2. destruct H2.
   eapply ClassesRefinementOK'; eauto.
 Qed.
-Hint Resolve ClassesRefinementOK  ClassesRefinementOK' pred_in_dom.
+Hint Resolve ClassesRefinementOK  ClassesRefinementOK' pred_in_dom'.
 
 
 Hypothesis ClassesOK: forall C CD,