made proof simpler

theories/GQMDeduction.v

@@ -47,20 +47,17 @@ Proof.
     apply/PeanoNat.Nat.ltb_spec0.
     omega.
   - move => n IH f A Hmaxv Himp.
-    have H := (gqm_Anec _ Himp).
+    have H := (gqm_Anec _ Himp); clear Himp.
     have HAmaxv : (n = max_var ([A] A)). {
       move => /=.
       rewrite -Hmaxv.
       omega.
     }
-    have H2 := (IH (switch_at n (fun k => f (S k)) (fun k => @ids _ Ids_form (S k))) _ HAmaxv H).
+    have H2 := (IH (fun k => f (S k)) _ HAmaxv H); clear H.
     asimpl in H2.
-    have H3 := (gqm_mp _ _ (gqm_AE _ (f 0)) H2).
+    have H3 := (gqm_mp _ _ (gqm_AE _ (f 0)) H2); clear H2.
     asimpl in H3.
-    rewrite (subst_end _ _ ids).
-    rewrite -Hmaxv.
-    (* Set Printing All. *)
-    suff <-: (f 0 .: switch_at n (fun n => f (S n)) (fun k => @ids _ Ids_form (S k)) = switch_at (S n) f (@ids _ Ids_form)) by [].
+    suff <-: (f 0 .: (fun k : var => f (S k)) = f) by [].
     apply: functional_extensionality => m.
     by case: m.
 Qed.
\ No newline at end of file