X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=8aa40051950869620b76f6e320f504ca2b547264;hp=8a49c81fe11368099b5e6acb29941aa2c68685b2;hb=db8c9d54c285980e162e393efd1b7316887e5b80;hpb=9241d797587022ecd51e3c38cd34588de6745524

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 8a49c81..8aa4005 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -6,6 +6,7 @@ Generalizable All Variables.
 Require Import Preamble.
 Require Import General.
 Require Import NaturalDeduction.
+Require Import NaturalDeductionContext.
 Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
@@ -15,20 +16,7 @@ Require Import HaskStrong.
 Require Import HaskProof.
 
 Section HaskStrongToProof.
-
-Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
-  RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
-
-Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
-  RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
-
-Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
-  eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
-  eapply RComp; [ idtac | apply RCossa ]. 
-  eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
-  apply RAssoc.
-  Defined.
-  
+ 
 Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
 (* maintenance of Xi *)