From 24cdfa08dee1c8c64d44b924486ef2a1433af539 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 4 Jan 2017 15:51:27 +0100
Subject: [PATCH] tweak proof

---
 theories/typing/function.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/typing/function.v b/theories/typing/function.v
index 877d7ff9..03efdebe 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -127,9 +127,8 @@ Section typing.
     Proper (pointwise_relation A (λ (v1 v2 : vec type n), Forall2 (eqtype E0 L0) v1 v2) ==>
             pointwise_relation A (eqtype E0 L0) ==> eqtype E0 L0) (fn E).
   Proof.
-    intros tys1 tys2 Htys ty1 ty2 Hty. split; eapply fn_subtype_ty'; try (by intro; apply Hty).
-    - intros x. eapply Forall2_flip, Forall2_impl; first by eapply (Htys x). by intros ??[].
-    - intros x. eapply Forall2_impl; first by eapply (Htys x). by intros ??[].
+    intros tys1 tys2 Htys ty1 ty2 Hty. split; eapply fn_subtype_ty'; try (by intro; apply Hty);
+      intros x; (apply Forall2_flip + idtac); (eapply Forall2_impl; first by eapply (Htys x)); by intros ??[].
   Qed.
 
   Lemma fn_subtype_elctx_sat {A n} E0 L0 E E' (tys : A → vec type n) ty :
-- 
GitLab