Fix use of iInduction, we had to generalize first.

TODO: fix Iris to generate better error messages.

theories/typing/function.v

@@ -275,14 +275,11 @@ Section typing.
       iDestruct (frac_bor_lft_incl with "LFT [>Hκs]") as "#Hκs".
       { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
       iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
-      + iApply "HE'". iFrame "#". iClear "Hf Hinh HE' LFT HE". clear.
-        (* FIXME: iInduction κs as [|κ κs] "IH". fails. *)
-        iRevert "Hκs". rewrite /coq_tactics.of_envs /=.
-        rewrite uPred.sep_elim_r. induction κs; iIntros "_ #Hκs"; simpl; first done.
+      + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
+        iInduction κs as [|κ κs] "IH" forall "Hκs"=> //=.
         iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
-        iApply IHκs; first by auto. iAlways.
-        iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
+        iApply "IH". iAlways. iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.
         iFrame "#∗".
       + iIntros (y) "IN". iDestruct "IN" as %->%elem_of_list_singleton.