Require Import Infrastructure.
Require Import Env.
Require Import Lia.
Require Import ProofIrrelevance.
Require Import Transp.
Require Import EquivarianceFacts.

Section Ind.

  Context {A: Type}
          (fVar: env A → atom → A → A)
          (fLetArg: ∀ (e: env A) (t: term) (a: A), A)
          (fLet: ∀ (e: env A) (t1: term) (a1: A) (x: atom) (t2: term) (a2: A), A)
          (fLamArg: env A → A)
          (fLam: ∀ (e: env A) (x: atom) (t: term) (a: A), A)
          (fApp: ∀ (e: env A) (t1: term) (a1: A) (t2: term) (a2: A), A)
          (fUnit: env A → A)
          (fPair: ∀ (e: env A) (t1: term) (a1: A) (t2: term) (a2: A), A)
          (fFst: ∀ (e: env A) (t: term) (a: A), A)
          (fSnd: ∀ (e: env A) (t: term) (a: A), A)
          (fInjL: ∀ (e: env A) (t: term) (a: A), A)
          (fInjR: ∀ (e: env A) (t: term) (a: A), A)
          (fMatchArg1: ∀ (e: env A) (t: term) (a: A), A)
          (fMatchArg2: ∀ (e: env A) (t: term) (a: A), A)
          (fMatch: ∀ (e: env A) (t: term) (a: A) (x1: atom) (t1: term) (a1: A) (x2: atom) (t2: term) (a2: A), A)
  .

  Section Ind0.

    Definition term_recurse0
               n (t: term)
               (Hsize: size t < n) (Hlc: lc t) (e: env A) (Hfv: fv t [<=] dom e)
    : A.
    Proof.
      revert t Hsize Hlc e Hfv.
      induction n; intros; [ abstract (exfalso; lia) | destruct t ].
      - abstract (exfalso; inversion Hlc).
      - assert A as a.
        { pose (get x e) as o.
          assert (get x e = o) as Heq.
          { subst o. reflexivity. }
          destruct o as [ a | ].
          - exact a.
          - abstract (exfalso; apply get_notin_dom in Heq; simpl in Hfv; fsetdec).
        }
        exact (fVar e x a).
      - assert A as a1.
        { apply IHn with (t := t1) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        pick fresh x for (dom e).
        assert A as a2.
        { apply IHn with (t := open t2 (Var x)) (e := x ¬ fLetArg e t1 a1 ++ e).
          - abstract (simpl in Hsize; rewrite size_open_var; lia).
          - abstract (inversion Hlc; subst; auto with lngen).
          - abstract (simpl in Hfv; rewrite fv_open_upper; simpl; fsetdec).
        }
        exact (fLet e t1 a1 x (open t2 (Var x)) a2).
      - pick fresh x for (dom e).
        assert A as a.
        { apply IHn with (t := open t (Var x)) (e := x ¬ fLamArg e ++ e).
          - abstract (simpl in Hsize; rewrite size_open_var; lia).
          - abstract (inversion Hlc; subst; auto with lngen).
          - abstract (simpl in Hfv; rewrite fv_open_upper; simpl; fsetdec).
        }
        exact (fLam e x (open t (Var x)) a).
      - assert A as a1.
        { apply IHn with (t := t1) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        assert A as a2.
        { apply IHn with (t := t2) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        exact (fApp e t1 a1 t2 a2).
      - exact (fUnit e).
      - assert A as a1.
        { apply IHn with (t := t1) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        assert A as a2.
        { apply IHn with (t := t2) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        exact (fPair e t1 a1 t2 a2).
      - assert A as a.
        { apply IHn with (t := t) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        exact (fFst e t a).
      - assert A as a.
        { apply IHn with (t := t) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        exact (fSnd e t a).
      - assert A as a.
        { apply IHn with (t := t) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        exact (fInjL e t a).
      - assert A as a.
        { apply IHn with (t := t) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        exact (fInjR e t a).
      - assert A as a1.
        { apply IHn with (t := t1) (e := e).
          - abstract (simpl in Hsize; lia).
          - abstract (inversion Hlc; assumption).
          - abstract (simpl in Hfv; fsetdec).
        }
        pick fresh x2 for (dom e).
        assert A as a2.
        { apply IHn with (t := open t2 (Var x2)) (e := x2 ¬ fMatchArg1 e t1 a1 ++ e).
          - abstract (simpl in Hsize; rewrite size_open_var; lia).
          - abstract (inversion Hlc; subst; auto with lngen).
          - abstract (simpl in Hfv; rewrite fv_open_upper; simpl; fsetdec).
        }
        pick fresh x3 for (dom e).
        assert A as a3.
        { apply IHn with (t := open t3 (Var x3)) (e := x3 ¬ fMatchArg2 e t1 a1 ++ e).
          - abstract (simpl in Hsize; rewrite size_open_var; lia).
          - abstract (inversion Hlc; subst; auto with lngen).
          - abstract (simpl in Hfv; rewrite fv_open_upper; simpl; fsetdec).
        }
        exact (fMatch e t1 a1 x2 (open t2 (Var x2)) a2 x3 (open t3 (Var x3)) a3).
    Defined.

    Lemma term_recurse0_proof_irrelevant
          n1 n2 t1 t2 (Heq: t1 = t2) (Hsize1: size t1 < n1) (Hsize2: size t2 < n2)
          (Hlc1: lc t1) (Hlc2: lc t2)
          (e1 e2: env A) (Heq_env: e1 = e2)
          (Hfv1: fv t1 [<=] dom e1) (Hfv2: fv t2 [<=] dom e2):
      term_recurse0 n1 t1 Hsize1 Hlc1 e1 Hfv1 = term_recurse0 n2 t2 Hsize2 Hlc2 e2 Hfv2.
    Proof.
      revert n2 t1 t2 Heq Hsize1 Hsize2 Hlc1 Hlc2 e1 e2 Heq_env Hfv1 Hfv2.
      induction n1; intros; [ exfalso; lia | destruct n2; [ lia |]; subst; destruct t2 ].
      - exfalso. inversion Hlc1.
      - simpl. f_equal. rewrite (proof_irrelevance _ Hfv1 Hfv2). reflexivity.
      - simpl. destruct (atom_fresh (dom e2)) as [x Fr]. f_equal.
        + apply IHn1; reflexivity.
        + apply IHn1; [ reflexivity |].
          f_equal. f_equal. f_equal. apply IHn1; reflexivity.
      - simpl. destruct (atom_fresh (dom e2)) as [x Fr]. f_equal.
        apply IHn1; reflexivity.
      - simpl. f_equal.
        + apply IHn1; reflexivity.
        + apply IHn1; reflexivity.
      - reflexivity.
      - simpl. f_equal.
        + apply IHn1; reflexivity.
        + apply IHn1; reflexivity.
      - simpl. f_equal. apply IHn1; reflexivity.
      - simpl. f_equal. apply IHn1; reflexivity.
      - simpl. f_equal. apply IHn1; reflexivity.
      - simpl. f_equal. apply IHn1; reflexivity.
      - simpl. destruct (atom_fresh (dom e2)) as [x Fr]. f_equal.
        + apply IHn1; reflexivity.
        + apply IHn1; [ reflexivity |].
          f_equal. f_equal. f_equal. apply IHn1; reflexivity.
        + apply IHn1; [ reflexivity |].
          f_equal. f_equal. f_equal. apply IHn1; reflexivity.
    Qed.

    Context (P: ∀ (e: env A) (t: term) (a: A), Prop)
            (HVar: ∀ (e: env A) x (Hx: x `in` dom e)
                     n (Hsize: size (Var x) < n)
                     (Hlc: lc (Var x))
                     (Hfv: fv (Var x) [<=] dom e)
                     (a: A) (Hget: get x e = Some a),
                P e (Var x) (fVar e x a)
            )
            (HLet: ∀ (e: env A) x (Hx: x `notin` dom e) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hsize2: size t2 < n) (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x (dom e)) a2
                    (Heq2: term_recurse0 n t2 Hsize2 Hlc2 (x ¬ fLetArg e t1 a1 ++ e) Hfv2 = a2)
                    (IH2: P (x ¬ fLetArg e t1 a1 ++ e) t2 a2),
                    ∀ (Hsize: size (Let t1 (close x t2)) < S n)
                      (Hlc: lc (Let t1 (close x t2)))
                      (Hfv: fv (Let t1 (close x t2)) [<=] dom e),
                      P e (Let t1 (close x t2)) (fLet e t1 a1 x t2 a2)
            )
            (HLam: ∀ (e: env A) x (Hx: x `notin` dom e) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] add x (dom e)) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 (x ¬ fLamArg e ++ e) Hfv1 = a1)
                  (IH1: P (x ¬ fLamArg e ++ e) t1 a1),
                  ∀ (Hsize: size (Lam (close x t1)) < S n)
                    (Hlc: lc (Lam (close x t1)))
                    (Hfv: fv (Lam (close x t1)) [<=] dom e),
                    P e (Lam (close x t1)) (fLam e x t1 a1)
            )
            (HApp: ∀ (e: env A) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hsize2: size t2 < n) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom e) a2
                    (Heq2: term_recurse0 n t2 Hsize2 Hlc2 e Hfv2 = a2)
                    (IH2: P e t2 a2),
                    ∀ (Hsize: size (App t1 t2) < S n)
                      (Hlc: lc (App t1 t2))
                      (Hfv: fv (App t1 t2) [<=] dom e),
                      P e (App t1 t2) (fApp e t1 a1 t2 a2)
            )
            (HUnit: ∀ (e: env A) n (Hsize: size Unit < n)
                      (Hlc: lc Unit)
                      (Hfv: fv Unit [<=] dom e),
                P e Unit (fUnit e)
            )
            (HPair: ∀ (e: env A) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hsize2: size t2 < n) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom e) a2
                    (Heq2: term_recurse0 n t2 Hsize2 Hlc2 e Hfv2 = a2)
                    (IH2: P e t2 a2),
                    ∀ (Hsize: size (Pair t1 t2) < S n)
                      (Hlc: lc (Pair t1 t2))
                      (Hfv: fv (Pair t1 t2) [<=] dom e),
                      P e (Pair t1 t2) (fPair e t1 a1 t2 a2)
            )
            (HFst: ∀ (e: env A) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hsize: size (Fst t1) < S n)
                    (Hlc: lc (Fst t1))
                    (Hfv: fv (Fst t1) [<=] dom e),
                    P e (Fst t1) (fFst e t1 a1)
            )
            (HSnd: ∀ (e: env A) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hsize: size (Snd t1) < S n)
                    (Hlc: lc (Snd t1))
                    (Hfv: fv (Snd t1) [<=] dom e),
                    P e (Snd t1) (fSnd e t1 a1)
            )
            (HInjL: ∀ (e: env A) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hsize: size (InjL t1) < S n)
                    (Hlc: lc (InjL t1))
                    (Hfv: fv (InjL t1) [<=] dom e),
                    P e (InjL t1) (fInjL e t1 a1)
            )
            (HInjR: ∀ (e: env A) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hsize: size (InjR t1) < S n)
                    (Hlc: lc (InjR t1))
                    (Hfv: fv (InjR t1) [<=] dom e),
                    P e (InjR t1) (fInjR e t1 a1)
            )
            (HMatch: ∀ (e: env A) x2 (Hx2: x2 `notin` dom e) x3 (Hx3: x3 `notin` dom e) n,
                ∀ t1 (Hsize1: size t1 < n) (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse0 n t1 Hsize1 Hlc1 e Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hsize2: size t2 < n) (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x2 (dom e)) a2
                    (Heq2: term_recurse0 n t2 Hsize2 Hlc2 (x2 ¬fMatchArg1 e t1 a1 ++ e) Hfv2 = a2)
                    (IH2: P (x2 ¬ fMatchArg1 e t1 a1 ++ e) t2 a2),
                    ∀ t3 (Hsize3: size t3 < n) (Hlc3: lc t3) (Hfv3: fv t3 [<=] add x3 (dom e)) a3
                      (Heq3: term_recurse0 n t3 Hsize3 Hlc3 (x3 ¬fMatchArg2 e t1 a1 ++ e) Hfv3 = a3)
                      (IH3: P (x3 ¬ fMatchArg2 e t1 a1 ++ e) t3 a3),
                      ∀ (Hsize: size (Match t1 (close x2 t2) (close x3 t3)) < S n)
                        (Hlc: lc (Match t1 (close x2 t2) (close x3 t3)))
                        (Hfv: fv (Match t1 (close x2 t2) (close x3 t3)) [<=] dom e),
                        P e (Match t1 (close x2 t2) (close x3 t3))
                          (fMatch e t1 a1 x2 t2 a2 x3 t3 a3)
            )
    .

    Lemma term_induction0
          n (t:term)
          (Hsize: size t < n) (Hlc: lc t) (e: env A) (Hfv: fv t [<=] dom e)
      : P e t (term_recurse0 n t Hsize Hlc e Hfv).
    Proof.
      revert t Hsize Hlc e Hfv.
      induction n; intros; [ exfalso; lia | destruct t ].
      - exfalso. inversion Hlc.
      - apply HVar with (n := S n); auto.
        + simpl in Hfv. fsetdec.
        + simpl.
          assert (∀ ox (Heq: get x e = ox),
                     ox =
                     Some
                       (match ox as o return (get x e = o → A) with
                        | Some a ⇒ fun _ : get x e = Some a ⇒ a
                        | None ⇒ fun Heq : get x e = None ⇒ term_recurse0_subproof1 x e Hfv Heq
                        end Heq)) as H.
          { intros ox Heq. destruct ox.
            + reflexivity.
            + exfalso. apply get_notin_dom in Heq. simpl in Hfv. fsetdec.
          }
          apply H.
      - simpl. destruct (atom_fresh (dom e)) as [x Fr].
        assert (x `notin` fv t2) as Hfv2.
        { simpl in Hfv. fsetdec. }
        revert Hsize Hlc Hfv.
        rewrite <- (close_open t2 x); [| assumption; clear Hfv2]; intros.
        erewrite (term_recurse0_proof_irrelevant n n (open (close x (open t2 (Var x))) (Var x)) (open t2 (Var x)) (open_close _ _) _ _ _ _ _ _ eq_refl).
        rewrite open_close.
        unshelve (eapply HLet with (n := S n); auto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst; assumption.
        + simpl in Hfv. fsetdec.
        + simpl in Hsize. rewrite size_close in Hsize. lia.
        + inversion Hlc. subst.
          specialize (H2 x). rewrite open_close in H2. assumption.
        + simpl in Hfv. rewrite fv_close in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
        + apply term_recurse0_proof_irrelevant; auto.
          Unshelve.
          × simpl in Hsize. rewrite size_close in Hsize. lia.
          × inversion Hlc. subst.
            specialize (H2 x). rewrite open_close in H2. assumption.
          × simpl. simpl in Hfv. rewrite fv_close in Hfv. fsetdec.
      - simpl. destruct (atom_fresh (dom e)) as [x Fr].
        assert (x `notin` fv t) as Hfv0.
        { simpl in Hfv. fsetdec. }
        revert Hsize Hlc Hfv.
        rewrite <- (close_open t x); [| assumption; clear Hfv0]; intros.
        erewrite (term_recurse0_proof_irrelevant n n (open (close x (open t (Var x))) (Var x)) (open t (Var x)) (open_close _ _) _ _ _ _ _ _ eq_refl).
        rewrite open_close.
        unshelve (eapply HLam with (n := S n); auto).
        + simpl in Hsize. rewrite size_close in Hsize. lia.
        + inversion Hlc; subst. specialize (H0 x). rewrite open_close in H0. assumption.
        + simpl in Hfv. rewrite fv_close in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
          Unshelve.
          × simpl in Hsize. rewrite size_close in Hsize. lia.
          × inversion Hlc; subst. specialize (H0 x). rewrite open_close in H0. assumption.
          × simpl. simpl in Hfv. rewrite fv_close in Hfv. fsetdec.
      - unshelve (eapply HApp with (n := S n); eauto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
        + apply term_recurse0_proof_irrelevant; auto.
      - apply HUnit with (n := S n). assumption.
        + auto.
        + simpl. auto.
      - unshelve (eapply HPair with (n := S n); eauto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
        + apply term_recurse0_proof_irrelevant; auto.
      - unshelve (eapply HFst with (n := S n); eauto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
      - unshelve (eapply HSnd with (n := S n); eauto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
      - unshelve (eapply HInjL with (n := S n); eauto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
      - unshelve (eapply HInjR with (n := S n); eauto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
      - simpl. destruct (atom_fresh (dom e)) as [x Fr].
        assert (x `notin` fv t2) as Hfv2.
        { simpl in Hfv. fsetdec. }
        revert Hsize Hlc Hfv.
        rewrite <- (close_open t2 x); [| assumption; clear Hfv2]; intros.
        assert (x `notin` fv t3) as Hfv3.
        { simpl in Hfv. fsetdec. }
        revert Hsize Hlc Hfv.
        rewrite <- (close_open t3 x); [| assumption; clear Hfv3]; intros.
        erewrite (term_recurse0_proof_irrelevant n n (open (close x (open t2 (Var x))) (Var x)) (open t2 (Var x)) (open_close _ _) _ _ _ _ _ _ eq_refl).
        erewrite (term_recurse0_proof_irrelevant n n (open (close x (open t3 (Var x))) (Var x)) (open t3 (Var x)) (open_close _ _) _ _ _ _ _ _ eq_refl).
        repeat rewrite open_close.
        unshelve (eapply HMatch with (n := S n); eauto).
        + simpl in Hsize. lia.
        + inversion Hlc; subst. assumption.
        + simpl in Hfv. fsetdec.
        + simpl in Hsize. repeat rewrite size_close in Hsize. lia.
        + inversion Hlc; subst. specialize (H3 x). rewrite open_close in H3. assumption.
        + simpl. simpl in Hfv. repeat rewrite fv_close in Hfv. fsetdec.
        + simpl in Hsize. repeat rewrite size_close in Hsize. lia.
        + inversion Hlc; subst. specialize (H4 x). rewrite open_close in H4. assumption.
        + simpl in Hfv. repeat rewrite fv_close in Hfv. fsetdec.
        + apply term_recurse0_proof_irrelevant; auto.
        + apply term_recurse0_proof_irrelevant; auto.
        + apply term_recurse0_proof_irrelevant; auto.
          Unshelve.
          × simpl in Hsize. repeat rewrite size_close in Hsize. lia.
          × inversion Hlc; subst. specialize (H3 x). rewrite open_close in H3. assumption.
          × simpl. simpl in Hfv. repeat rewrite fv_close in Hfv. fsetdec.
          × simpl in Hsize. repeat rewrite size_close in Hsize. lia.
          × inversion Hlc; subst. specialize (H4 x). rewrite open_close in H4. assumption.
          × simpl. simpl in Hfv. repeat rewrite fv_close in Hfv. fsetdec.
    Qed.

  End Ind0.

  Definition term_recurse (e: env A) (t: term) (Hlc: lc t) (Hfv: fv t [<=] dom e) : A.
  Proof.
    apply (term_recurse0 (S (size t)) t) with (e := e).
    - abstract lia.
    - assumption.
    - assumption.
  Defined.

  Lemma term_recurse_proof_irrelevant
        (e1 e2: env A) (Heq_env: e1 = e2)
        (t1 t2: term) (Heq: t1 = t2)
        (Hlc1: lc t1) (Hlc2: lc t2)
        (Hfv1: fv t1 [<=] dom e1) (Hfv2: fv t2 [<=] dom e2) :
    term_recurse e1 t1 Hlc1 Hfv1 = term_recurse e2 t2 Hlc2 Hfv2.
  Proof.
    unfold term_recurse.
    apply term_recurse0_proof_irrelevant; assumption.
  Qed.

  Lemma term_recurse_equations (e: env A) (t: term) (Hlc: lc t) (Hfv: fv t [<=] dom e) :
    match t with
    | BVar _ ⇒ False
    | Var x ⇒ ∃ a, get x e = Some a ∧ term_recurse e t Hlc Hfv = fVar e x a
    | Let t1 t2 ⇒
      ∃ x (Hx: x `notin` dom e) t2' (Heq: t2 = close x t2')
        (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e)
        (Hlc2: lc t2') (Hfv2: fv t2' [<=] add x (dom e)),
      term_recurse e t Hlc Hfv =
      let a1 := term_recurse e t1 Hlc1 Hfv1 in
      let a2 := term_recurse (x ¬ fLetArg e t1 a1 ++ e) t2' Hlc2 Hfv2 in
      fLet e t1 a1 x (open t2 (Var x)) a2
    | Lam t1 ⇒
      ∃ x (Hx: x `notin` dom e) t1' (Heq: t1 = close x t1')
        (Hlc1: lc t1') (Hfv1: fv t1' [<=] add x (dom e)),
      term_recurse e t Hlc Hfv =
      fLam e x t1' (term_recurse (x ¬ fLamArg e ++ e) t1' Hlc1 Hfv1)
    | App t1 t2 ⇒
      ∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom e),
      term_recurse e t Hlc Hfv =
      fApp e t1 (term_recurse e t1 Hlc1 Hfv1) t2 (term_recurse e t2 Hlc2 Hfv2)
    | Unit ⇒ term_recurse e t Hlc Hfv = fUnit e
    | Pair t1 t2 ⇒
      ∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom e),
      term_recurse e t Hlc Hfv =
      fPair e t1 (term_recurse e t1 Hlc1 Hfv1) t2 (term_recurse e t2 Hlc2 Hfv2)
    | Fst t1 ⇒
      ∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e),
      term_recurse e t Hlc Hfv = fFst e t1 (term_recurse e t1 Hlc1 Hfv1)
    | Snd t1 ⇒
      ∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e),
      term_recurse e t Hlc Hfv = fSnd e t1 (term_recurse e t1 Hlc1 Hfv1)
    | InjL t1 ⇒
      ∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e),
      term_recurse e t Hlc Hfv = fInjL e t1 (term_recurse e t1 Hlc1 Hfv1)
    | InjR t1 ⇒
      ∃ (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e),
      term_recurse e t Hlc Hfv = fInjR e t1 (term_recurse e t1 Hlc1 Hfv1)
    | Match t0 t1 t2 ⇒
      ∃ x1 (Hx1: x1 `notin` dom e) t1' (Heq: t1 = close x1 t1')
        x2 (Hx2: x2 `notin` dom e) t2' (Heq: t2 = close x2 t2')
        (Hlc0: lc t0) (Hfv0: fv t0 [<=] dom e)
        (Hlc1: lc t1') (Hfv1: fv t1' [<=] add x1 (dom e))
        (Hlc2: lc t2') (Hfv2: fv t2' [<=] add x2 (dom e)),
      term_recurse e t Hlc Hfv =
      let a0 := term_recurse e t0 Hlc0 Hfv0 in
      let a1 := term_recurse (x1 ¬ fMatchArg1 e t0 a0 ++ e) t1' Hlc1 Hfv1 in
      let a2 := term_recurse (x2 ¬ fMatchArg2 e t0 a0 ++ e) t2' Hlc2 Hfv2 in
      fMatch e t0 a0 x1 t1' a1 x2 t2' a2
    end.
  Proof.
    destruct t.
    - inversion Hlc.
    - case_eq (get x e); intros.
      + ∃ a. split; [ reflexivity |].
        unfold term_recurse. simpl. f_equal.
        assert (∀ y,
                   y = get x e →
                   ∀ (Heq: get x e = y),
                     match y as o return (get x e = o → A) with
                     | Some a0 ⇒ fun _ : get x e = Some a0 ⇒ a0
                     | None ⇒ fun Heq : get x e = None ⇒ term_recurse0_subproof1 x e Hfv Heq
                     end Heq = a).
        { intros y Hy Heq. destruct y; congruence. }
        apply (H0 (get x e) eq_refl).
      + exfalso. apply get_notin_dom in H. simpl in Hfv. fsetdec.
    - case_eq (atom_fresh (dom e)); intros x Fr Heqx.
      assert (t2 = close x (open t2 (Var x))) as Heq.
      { simpl in Hfv. rewrite close_open; auto. }
      assert (lc t1 ∧ lc (open t2 (Var x))) as [Hlc1 Hlc2].
      { inversion Hlc; subst. auto. }
      assert (fv t1 [<=] dom e ∧ fv (open t2 (Var x)) [<=] add x (dom e)) as [Hfv1 Hfv2].
      { simpl in Hfv. split. fsetdec. rewrite fv_open_upper. simpl. fsetdec. }
      ∃ x, Fr, (open t2 (Var x)), Heq, Hlc1, Hfv1, Hlc2, Hfv2.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2)) t1 t1 eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2)) (open t2 (Var x)) (open t2 (Var x)) eq_refl
           _ _ _ _
           _ (x ¬ fLetArg e t1 _ ++ e) _
           _ _).
      unfold term_recurse. simpl. rewrite Heqx. f_equal.
      Unshelve.
      + simpl. rewrite Heqx. reflexivity.
    - case_eq (atom_fresh (dom e)); intros x Fr Heqx.
      assert (t = close x (open t (Var x))) as Heq.
      { simpl in Hfv. rewrite close_open; auto. }
      assert (lc (open t (Var x))) as Hlc1.
      { inversion Hlc; subst. auto. }
      assert (fv (open t (Var x)) [<=] add x (dom e)) as Hfv1.
      { simpl in Hfv. rewrite fv_open_upper. simpl. fsetdec. }
      ∃ x, Fr, (open t (Var x)), Heq, Hlc1, Hfv1.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t)) (open t (Var x)) (open t (Var x)) eq_refl
           _ _ _ _
           _ (x ¬ fLamArg e ++ e) _
           _ _).
      unfold term_recurse. simpl. rewrite Heqx. f_equal.
      Unshelve.
      + reflexivity.
    - assert (lc t1 ∧ lc t2) as [Hlc1 Hlc2].
      { inversion Hlc; subst. auto. }
      assert (fv t1 [<=] dom e ∧ fv t2 [<=] dom e) as [Hfv1 Hfv2].
      { simpl in Hfv. split; fsetdec. }
      ∃ Hlc1, Hfv1, Hlc2, Hfv2.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2)) t1 t1 eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2)) t2 t2 eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      reflexivity.
    - reflexivity.
    - assert (lc t1 ∧ lc t2) as [Hlc1 Hlc2].
      { inversion Hlc; subst. auto. }
      assert (fv t1 [<=] dom e ∧ fv t2 [<=] dom e) as [Hfv1 Hfv2].
      { simpl in Hfv. split; fsetdec. }
      ∃ Hlc1, Hfv1, Hlc2, Hfv2.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2)) t1 t1 eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2)) t2 t2 eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      reflexivity.
    - assert (lc t) as Hlc1.
      { inversion Hlc; subst. auto. }
      ∃ Hlc1, Hfv.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t)) t t eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      reflexivity.
    - assert (lc t) as Hlc1.
      { inversion Hlc; subst. auto. }
      ∃ Hlc1, Hfv.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t)) t t eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      reflexivity.
    - assert (lc t) as Hlc1.
      { inversion Hlc; subst. auto. }
      ∃ Hlc1, Hfv.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t)) t t eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      reflexivity.
    - assert (lc t) as Hlc1.
      { inversion Hlc; subst. auto. }
      ∃ Hlc1, Hfv.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t)) t t eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      reflexivity.
    - case_eq (atom_fresh (dom e)); intros x Fr Heqx.
      assert (t2 = close x (open t2 (Var x))) as Heq2.
      { simpl in Hfv. rewrite close_open; fsetdec. }
      assert (t3 = close x (open t3 (Var x))) as Heq3.
      { simpl in Hfv. rewrite close_open; fsetdec. }
      assert (lc t1 ∧ lc (open t2 (Var x)) ∧ lc (open t3 (Var x))) as [Hlc1 [Hlc2 Hlc3]].
      { inversion Hlc; subst. auto. }
      assert (fv t1 [<=] dom e
              ∧ fv (open t2 (Var x)) [<=] add x (dom e)
              ∧ fv (open t3 (Var x)) [<=] add x (dom e))
        as [Hfv1 [Hfv2 Hfv3]].
      { simpl in Hfv. split. fsetdec. split; rewrite fv_open_upper; simpl; fsetdec. }
      ∃ x, Fr, (open t2 (Var x)), Heq2, x, Fr, (open t3 (Var x)), Heq3,
      Hlc1, Hfv1, Hlc2, Hfv2, Hlc3, Hfv3.
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2 + size t3)) t1 t1 eq_refl
           _ _ _ _
           e e eq_refl
           _ _).
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2 + size t3)) (open t2 (Var x)) (open t2 (Var x)) eq_refl
           _ _ _ _
           _ (x ¬ fMatchArg1 e t1 _ ++ e) _
           _ _).
      unfold term_recurse at 2.
      erewrite
        (term_recurse0_proof_irrelevant
           _ (S (size t1 + size t2 + size t3)) (open t3 (Var x)) (open t3 (Var x)) eq_refl
           _ _ _ _
           _ (x ¬ fMatchArg2 e t1 _ ++ e) _
           _ _).
      unfold term_recurse. simpl. rewrite Heqx. f_equal.
      Unshelve.
      + simpl. rewrite Heqx. reflexivity.
      + simpl. rewrite Heqx. reflexivity.
  Qed.

  Section Ind.

    Context (P: ∀ (e: env A) (t: term) (a: A), Prop)
            (HVar: ∀ (e: env A) x (Hx: x `in` dom e)
                     (Hlc: lc (Var x))
                     (Hfv: fv (Var x) [<=] dom e)
                     (a: A) (Hget: get x e = Some a),
                P e (Var x) (fVar e x a)
            )
            (HLet: ∀ (e: env A) x (Hx: x `notin` dom e),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x (dom e)) a2
                    (Heq2: term_recurse (x ¬ fLetArg e t1 a1 ++ e) t2 Hlc2 Hfv2 = a2)
                    (IH2: P (x ¬ fLetArg e t1 a1 ++ e) t2 a2),
                    ∀ (Hlc: lc (Let t1 (close x t2)))
                      (Hfv: fv (Let t1 (close x t2)) [<=] dom e),
                      P e (Let t1 (close x t2)) (fLet e t1 a1 x t2 a2)
            )
            (HLam: ∀ (e: env A) x (Hx: x `notin` dom e),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] add x (dom e)) a1
                  (Heq1: term_recurse (x ¬ fLamArg e ++ e) t1 Hlc1 Hfv1 = a1)
                  (IH1: P (x ¬ fLamArg e ++ e) t1 a1),
                  ∀ (Hlc: lc (Lam (close x t1)))
                    (Hfv: fv (Lam (close x t1)) [<=] dom e),
                    P e (Lam (close x t1)) (fLam e x t1 a1)
            )
            (HApp: ∀ (e: env A),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom e) a2
                    (Heq2: term_recurse e t2 Hlc2 Hfv2 = a2)
                    (IH2: P e t2 a2),
                    ∀ (Hlc: lc (App t1 t2))
                      (Hfv: fv (App t1 t2) [<=] dom e),
                      P e (App t1 t2) (fApp e t1 a1 t2 a2)
            )
            (HUnit: ∀ (e: env A) (Hlc: lc Unit) (Hfv: fv Unit [<=] dom e),
                P e Unit (fUnit e)
            )
            (HPair: ∀ (e: env A),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] dom e) a2
                    (Heq2: term_recurse e t2 Hlc2 Hfv2 = a2)
                    (IH2: P e t2 a2),
                    ∀ (Hlc: lc (Pair t1 t2))
                           (Hfv: fv (Pair t1 t2) [<=] dom e),
                      P e (Pair t1 t2) (fPair e t1 a1 t2 a2)
            )
            (HFst: ∀ (e: env A),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hlc: lc (Fst t1)) (Hfv: fv (Fst t1) [<=] dom e),
                    P e (Fst t1) (fFst e t1 a1)
            )
            (HSnd: ∀ (e: env A),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hlc: lc (Snd t1)) (Hfv: fv (Snd t1) [<=] dom e),
                    P e (Snd t1) (fSnd e t1 a1)
            )
            (HInjL: ∀ (e: env A),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hlc: lc (InjL t1)) (Hfv: fv (InjL t1) [<=] dom e),
                    P e (InjL t1) (fInjL e t1 a1)
            )
            (HInjR: ∀ (e: env A),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ (Hlc: lc (InjR t1)) (Hfv: fv (InjR t1) [<=] dom e),
                    P e (InjR t1) (fInjR e t1 a1)
            )
            (HMatch: ∀ (e: env A) x2 (Hx2: x2 `notin` dom e) x3 (Hx3: x3 `notin` dom e),
                ∀ t1 (Hlc1: lc t1) (Hfv1: fv t1 [<=] dom e) a1
                  (Heq1: term_recurse e t1 Hlc1 Hfv1 = a1)
                  (IH1: P e t1 a1),
                  ∀ t2 (Hlc2: lc t2) (Hfv2: fv t2 [<=] add x2 (dom e)) a2
                    (Heq2: term_recurse (x2 ¬ fMatchArg1 e t1 a1 ++ e) t2 Hlc2 Hfv2 = a2)
                    (IH2: P (x2 ¬ fMatchArg1 e t1 a1 ++ e) t2 a2),
                    ∀ t3 (Hlc3: lc t3) (Hfv3: fv t3 [<=] add x3 (dom e)) a3
                      (Heq3: term_recurse (x3 ¬ fMatchArg2 e t1 a1 ++ e) t3 Hlc3 Hfv3 = a3)
                      (IH3: P (x3 ¬ fMatchArg2 e t1 a1 ++ e) t3 a3),
                      ∀ (Hlc: lc (Match t1 (close x2 t2) (close x3 t3)))
                        (Hfv: fv (Match t1 (close x2 t2) (close x3 t3)) [<=] dom e),
                        P e (Match t1 (close x2 t2) (close x3 t3))
                          (fMatch e t1 a1 x2 t2 a2 x3 t3 a3)
            )
    .