X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=d9c6a7eef94758a8327913aa74aa3b2c71a4afda;hp=ee536b01cd63666b6c3835d788b21f26a3bbbac5;hb=93ac0d63048027161f816c451a7954fb8a6470c0;hpb=6ae1b9b08da7c1d1f0de42afa1ccbf42acda3e62

diff --git a/src/HaskProof.v b/src/HaskProof.v
index ee536b0..d9c6a7e 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -45,6 +45,7 @@ Implicit Arguments ProofCaseBranch [ ].
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)
 Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
+| RId     : forall a        ,                Arrange           a                  a
 | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
 | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
 | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
@@ -176,6 +177,7 @@ Definition arrangeMap :
     Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
   intros.
   induction X; simpl.
+  apply RId.
   apply RCanL.
   apply RCanR.
   apply RuCanL.