swap order of hypotheses in RApp to match RLet

[coq-hetmet.git] / src / HaskProof.v

diff --git a/src/HaskProof.v b/src/HaskProof.v
index d28db62..ee536b0 100644 (file)
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -81,7 +81,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 | RJoin  : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ ,   Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ])         [Γ>Δ>  Σ₁,,Σ₂  |- τ₁,,τ₂          ]
 
-| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁       |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
+| RApp           : ∀ Γ Δ Σ₁ Σ₂ tx te l,  Rule ([Γ>Δ> Σ₁ |- [tx@@l]],,[Γ>Δ> Σ₂       |- [tx--->te @@l]])  [Γ>Δ> Σ₁,,Σ₂ |- [te   @@l]]
 
 | RLet           : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,  Rule ([Γ>Δ> Σ₂ |- [σ₂@@l]],,[Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ])     [Γ>Δ> Σ₁,,Σ₂ |- [σ₁   @@l]]