Documentation

Auto.Embedding.LamBase

Interpreted sorts

Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Auto.Embedding.Lam.LamBaseSort.eq_of_beq_eq_true {b₁ b₂ : LamBaseSort} :
      b₁.beq b₂ = trueb₁ = b₂
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          Instances For

            Given a and [ty₀, ty₁, ⋯, tyᵢ₋₁], return ty₀ → ty₁ → ⋯ → tyᵢ₋₁ → a

            Equations
            Instances For
              theorem Auto.Embedding.Lam.LamSort.mkFuncs_cons {a ty : LamSort} {tys : List LamSort} :
              a.mkFuncs (ty :: tys) = ty.func (a.mkFuncs tys)
              theorem Auto.Embedding.Lam.LamSort.mkFuncs_append {a : LamSort} {tys₁ tys₂ : List LamSort} :
              a.mkFuncs (tys₁ ++ tys₂) = (a.mkFuncs tys₂).mkFuncs tys₁

              Given a and [ty₀, ty₁, ⋯, tyᵢ₋₁], return tyᵢ₋₁ → ⋯ → ty₁ → ty₀ → a

              Equations
              Instances For

                Given ty₀ → ty₁ → ⋯ → tyᵢ₋₁ → a, return [ty₀, ty₁, ⋯, tyᵢ₋₁]

                Equations
                Instances For

                  Given ty₀ → ty₁ → ⋯ → tyₙ₋₁ → a, return [ty₀, ty₁, ⋯, tyₙ₋₁]

                  Equations
                  Instances For
                    theorem Auto.Embedding.Lam.LamSort.getArgTysN_getResTyN_eq {n : Nat} {s : LamSort} {l : List LamSort} {s' : LamSort} (hArg : getArgTysN n s = some l) (hRes : getResTyN n s = some s') :
                    s = s'.mkFuncs l
                    def Auto.Embedding.Lam.LamSort.curry {tyVal : NatType u_1} {tys : List LamSort} {s : LamSort} (f : HList (interp tyVal) tysinterp tyVal s) :
                    interp tyVal (s.mkFuncs tys)
                    Equations
                    Instances For
                      def Auto.Embedding.Lam.LamSort.curryRev {tyVal : NatType u_1} {tys : List LamSort} {s : LamSort} (f : HList (interp tyVal) tysinterp tyVal s) :
                      interp tyVal (s.mkFuncsRev tys)
                      Equations
                      Instances For
                        Instances For
                          Equations
                          Instances For
                            Equations
                            • =
                            Instances For
                              def Auto.Embedding.Lam.PropConst.eq_of_beq_eq_true {p₁ p₂ : PropConst} (H : p₁.beq p₂ = true) :
                              p₁ = p₂
                              Equations
                              • =
                              Instances For
                                def Auto.Embedding.Lam.PropConst.LamWF.unique {p : PropConst} {s₁ s₂ : LamSort} (pcwf₁ : p.LamWF s₁) (pcwf₂ : p.LamWF s₂) :
                                s₁ = s₂ pcwf₁ pcwf₂
                                Equations
                                • =
                                Instances For
                                  Equations
                                  • =
                                  Instances For
                                    Equations
                                    • =
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            • =
                                            Instances For
                                              def Auto.Embedding.Lam.BoolConst.eq_of_beq_eq_true {b₁ b₂ : BoolConst} (H : b₁.beq b₂ = true) :
                                              b₁ = b₂
                                              Equations
                                              • =
                                              Instances For
                                                def Auto.Embedding.Lam.BoolConst.LamWF.unique {b : BoolConst} {s₁ s₂ : LamSort} (bcwf₁ : b.LamWF s₁) (bcwf₂ : b.LamWF s₂) :
                                                s₁ = s₂ bcwf₁ bcwf₂
                                                Equations
                                                • =
                                                Instances For
                                                  Equations
                                                  • =
                                                  Instances For
                                                    Equations
                                                    • =
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Instances For
                                                          Equations
                                                          Instances For
                                                            Equations
                                                            • =
                                                            Instances For
                                                              def Auto.Embedding.Lam.NatConst.eq_of_beq_eq_true {n₁ n₂ : NatConst} (H : n₁.beq n₂ = true) :
                                                              n₁ = n₂
                                                              Equations
                                                              • =
                                                              Instances For
                                                                def Auto.Embedding.Lam.NatConst.LamWF.unique {n : NatConst} {s₁ s₂ : LamSort} (nwf₁ : n.LamWF s₁) (nwf₂ : n.LamWF s₂) :
                                                                s₁ = s₂ nwf₁ nwf₂
                                                                Equations
                                                                • =
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Equations
                                                                    • =
                                                                    Instances For
                                                                      Equations
                                                                      • =
                                                                      Instances For
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          Instances For
                                                                            Equations
                                                                            Instances For
                                                                              Equations
                                                                              • =
                                                                              Instances For
                                                                                def Auto.Embedding.Lam.IntConst.eq_of_beq_eq_true {i₁ i₂ : IntConst} (H : i₁.beq i₂ = true) :
                                                                                i₁ = i₂
                                                                                Equations
                                                                                • =
                                                                                Instances For
                                                                                  Instances For
                                                                                    def Auto.Embedding.Lam.IntConst.LamWF.unique {i : IntConst} {s₁ s₂ : LamSort} (iwf₁ : i.LamWF s₁) (iwf₂ : i.LamWF s₂) :
                                                                                    s₁ = s₂ iwf₁ iwf₂
                                                                                    Equations
                                                                                    • =
                                                                                    Instances For
                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        Equations
                                                                                        • =
                                                                                        Instances For
                                                                                          Equations
                                                                                          • =
                                                                                          Instances For
                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              Instances For
                                                                                                Equations
                                                                                                Instances For
                                                                                                  Equations
                                                                                                  • =
                                                                                                  Instances For
                                                                                                    def Auto.Embedding.Lam.StringConst.eq_of_beq_eq_true {s₁ s₂ : StringConst} (H : s₁.beq s₂ = true) :
                                                                                                    s₁ = s₂
                                                                                                    Equations
                                                                                                    • =
                                                                                                    Instances For
                                                                                                      def Auto.Embedding.Lam.StringConst.LamWF.unique {s : StringConst} {s₁ s₂ : LamSort} (iwf₁ : s.LamWF s₁) (iwf₂ : s.LamWF s₂) :
                                                                                                      s₁ = s₂ iwf₁ iwf₂
                                                                                                      Equations
                                                                                                      • =
                                                                                                      Instances For
                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          Equations
                                                                                                          • =
                                                                                                          Instances For
                                                                                                            Equations
                                                                                                            • =
                                                                                                            Instances For
                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                Instances For
                                                                                                                  Equations
                                                                                                                  • =
                                                                                                                  Instances For
                                                                                                                    def Auto.Embedding.Lam.BVAOp.eq_of_beq_eq_true {a₁ a₂ : BVAOp} (H : a₁.beq a₂ = true) :
                                                                                                                    a₁ = a₂
                                                                                                                    Equations
                                                                                                                    • =
                                                                                                                    Instances For
                                                                                                                      Instances For
                                                                                                                        Equations
                                                                                                                        • =
                                                                                                                        Instances For
                                                                                                                          def Auto.Embedding.Lam.BVCmp.eq_of_beq_eq_true {c₁ c₂ : BVCmp} (H : c₁.beq c₂ = true) :
                                                                                                                          c₁ = c₂
                                                                                                                          Equations
                                                                                                                          • =
                                                                                                                          Instances For
                                                                                                                            Instances For
                                                                                                                              Equations
                                                                                                                              • =
                                                                                                                              Instances For
                                                                                                                                def Auto.Embedding.Lam.BVShOp.eq_of_beq_eq_true {s₁ s₂ : BVShOp} (H : s₁.beq s₂ = true) :
                                                                                                                                s₁ = s₂
                                                                                                                                Equations
                                                                                                                                • =
                                                                                                                                Instances For

                                                                                                                                  Following https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV

                                                                                                                                  Instances For
                                                                                                                                    Equations
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                      Instances For
                                                                                                                                        Equations
                                                                                                                                        Instances For
                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            Equations
                                                                                                                                            • =
                                                                                                                                            Instances For
                                                                                                                                              def Auto.Embedding.Lam.BitVecConst.eq_of_beq_eq_true {b₁ b₂ : BitVecConst} (H : b₁.beq b₂ = true) :
                                                                                                                                              b₁ = b₂
                                                                                                                                              Equations
                                                                                                                                              • =
                                                                                                                                              Instances For
                                                                                                                                                Instances For
                                                                                                                                                  def Auto.Embedding.Lam.BitVecConst.LamWF.unique {b : BitVecConst} {s₁ s₂ : LamSort} (bcwf₁ : b.LamWF s₁) (bcwf₂ : b.LamWF s₂) :
                                                                                                                                                  s₁ = s₂ bcwf₁ bcwf₂
                                                                                                                                                  Equations
                                                                                                                                                  • =
                                                                                                                                                  Instances For
                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For
                                                                                                                                                      Equations
                                                                                                                                                      • =
                                                                                                                                                      Instances For
                                                                                                                                                        Equations
                                                                                                                                                        • =
                                                                                                                                                        Instances For
                                                                                                                                                          Equations
                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                          Instances For
                                                                                                                                                            • smtAttr1T : StringLamSortLamSortOtherConst

                                                                                                                                                              SMT attribute application, with one term as ⟨attribute_value⟩ .app _ (attribute ⟨keyword⟩ ⟨attr_term⟩) ⟨term⟩ ⇔ ⟨term⟩ ⟨keyword⟩ (⟨attr_term⟩)

                                                                                                                                                              smtAttr1T n s₁ s₂ is interpreted as fun (_ : s₁) (x₂ : s₂) => x₂, which we'll denote as constId. Note that the interpretation is polymorphic. However, it does not need special treatment like ∀, ∃, =. This is because constId A↑ B↑ = (constId A B)↑, where stands for universe level lifting.

                                                                                                                                                            Instances For
                                                                                                                                                              Equations
                                                                                                                                                              Instances For
                                                                                                                                                                Instances For
                                                                                                                                                                  Equations
                                                                                                                                                                  Instances For
                                                                                                                                                                    Equations
                                                                                                                                                                    • =
                                                                                                                                                                    Instances For
                                                                                                                                                                      def Auto.Embedding.Lam.OtherConst.eq_of_beq_eq_true {o₁ o₂ : OtherConst} (H : o₁.beq o₂ = true) :
                                                                                                                                                                      o₁ = o₂
                                                                                                                                                                      Equations
                                                                                                                                                                      • =
                                                                                                                                                                      Instances For
                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          def Auto.Embedding.Lam.OtherConst.interp_equiv {p : OtherConst} {s : LamSort} (tyVal : NatType u) (ocwf : p.LamWF s) :
                                                                                                                                                                          LamWF.interp tyVal ocwf interp tyVal p
                                                                                                                                                                          Equations
                                                                                                                                                                          • =
                                                                                                                                                                          Instances For
                                                                                                                                                                            def Auto.Embedding.Lam.OtherConst.LamWF.unique {o : OtherConst} {s₁ s₂ : LamSort} (ocwf₁ : o.LamWF s₁) (ocwf₂ : o.LamWF s₂) :
                                                                                                                                                                            s₁ = s₂ ocwf₁ ocwf₂
                                                                                                                                                                            Equations
                                                                                                                                                                            • =
                                                                                                                                                                            Instances For
                                                                                                                                                                              theorem Auto.Embedding.Lam.OtherConst.LamWF.interp_lvalIrrelevance {b₁ : OtherConst} {s₁ : LamSort} {b₂ : OtherConst} {s₂ : LamSort} (tyVal₁ tyVal₂ : NatType u) (ocwf₁ : b₁.LamWF s₁) (ocwf₂ : b₂.LamWF s₂) (HBeq : b₁ = b₂) (hTyVal : tyVal₁ = tyVal₂) :
                                                                                                                                                                              interp tyVal₁ ocwf₁ interp tyVal₂ ocwf₂
                                                                                                                                                                              Equations
                                                                                                                                                                              • =
                                                                                                                                                                              Instances For
                                                                                                                                                                                Equations
                                                                                                                                                                                • =
                                                                                                                                                                                Instances For
                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For

                                                                                                                                                                                    Interpreted constants Note that eq, forallE, existE have ilVal/lamILTy associated with them. During proof reconstruction, we should collect the sort arguments of all eq, forallE, existE that occurs in the proof into ilVal. For ilVal, we need to use ILLift.ofIsomTy to construct ILLift structures. The idea is that we want the interpretation of reified assumptions to be definitionally equal to the assumption (or GLift.up applied to the assumption, to be precise), so we'll have to use the specially designed of(Eq/Forall/Exist)Lift function. Note that at the end of the proof, we'll have a LamTerm.base .falseE, no =, ∀, ∃ left, so whatever (Eq/Forall/Exist)Lift structure are within the (eq/forall/lam)Val, the final result will always interpret to GLift.up False.

                                                                                                                                                                                    Instances For
                                                                                                                                                                                      Equations
                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          Equations
                                                                                                                                                                                          • =
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            def Auto.Embedding.Lam.LamBaseTerm.eq_of_beq_eq_true {b₁ b₂ : LamBaseTerm} (H : b₁.beq b₂ = true) :
                                                                                                                                                                                            b₁ = b₂
                                                                                                                                                                                            Equations
                                                                                                                                                                                            • =
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For
                                                                                                                                                                                                  def Auto.Embedding.Lam.LamBaseTerm.LamWF.unique {ltv : LamTyVal} {b : LamBaseTerm} {s₁ s₂ : LamSort} (lbwf₁ : LamWF ltv b s₁) (lbwf₂ : LamWF ltv b s₂) :
                                                                                                                                                                                                  s₁ = s₂ lbwf₁ lbwf₂
                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • =
                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                    def Auto.Embedding.Lam.LamBaseTerm.LamWF.eVarIrrelevance {ltv₁ : LamTyVal} {b : LamBaseTerm} {s : LamSort} {ltv₂ : LamTyVal} (hLamVarTy : ltv₁.lamVarTy = ltv₂.lamVarTy) (hLamILTy : ltv₁.lamILTy = ltv₂.lamILTy) (lbwf : LamWF ltv₁ b s) :
                                                                                                                                                                                                    LamWF ltv₂ b s
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      Equations
                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                        Equations
                                                                                                                                                                                                        • =
                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                          Equations
                                                                                                                                                                                                          • =
                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                            Equations
                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                              structure Auto.Embedding.Lam.ILLift (β : Type u) :
                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                noncomputable def Auto.Embedding.Lam.ILLift.ofIsomTy {α : Sort u} {β : Type v} (I : IsomType α β) :
                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                  noncomputable def Auto.Embedding.Lam.ILLift.default (β : Type u) :
                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                      theorem Auto.Embedding.Lam.PropConst.LamWF.interp_lvalIrrelevance {p₁ : PropConst} {s₁ : LamSort} {p₂ : PropConst} {s₂ : LamSort} (tyVal₁ tyVal₂ : NatType u) (pcwf₁ : p₁.LamWF s₁) (pcwf₂ : p₂.LamWF s₂) (HBeq : p₁ = p₂) (hTyVal : tyVal₁ = tyVal₂) :
                                                                                                                                                                                                                      interp tyVal₁ pcwf₁ interp tyVal₂ pcwf₂
                                                                                                                                                                                                                      def Auto.Embedding.Lam.PropConst.interp_equiv {p : PropConst} {s : LamSort} (tyVal : NatType u) (pcwf : p.LamWF s) :
                                                                                                                                                                                                                      LamWF.interp tyVal pcwf interp tyVal p
                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                      • =
                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                        theorem Auto.Embedding.Lam.BoolConst.LamWF.interp_lvalIrrelevance {b₁ : BoolConst} {s₁ : LamSort} {b₂ : BoolConst} {s₂ : LamSort} (tyVal₁ tyVal₂ : NatType u) (bcwf₁ : b₁.LamWF s₁) (bcwf₂ : b₂.LamWF s₂) (HBeq : b₁ = b₂) (hTyVal : tyVal₁ = tyVal₂) :
                                                                                                                                                                                                                        interp tyVal₁ bcwf₁ interp tyVal₂ bcwf₂
                                                                                                                                                                                                                        def Auto.Embedding.Lam.BoolConst.interp_equiv {b : BoolConst} {s : LamSort} (tyVal : NatType u) (bcwf : b.LamWF s) :
                                                                                                                                                                                                                        LamWF.interp tyVal bcwf interp tyVal b
                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                        • =
                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                          theorem Auto.Embedding.Lam.NatConst.LamWF.interp_lvalIrrelevance {n₁ : NatConst} {s₁ : LamSort} {n₂ : NatConst} {s₂ : LamSort} (tyVal₁ tyVal₂ : NatType u) (ncwf₁ : n₁.LamWF s₁) (ncwf₂ : n₂.LamWF s₂) (HBeq : n₁ = n₂) (hTyVal : tyVal₁ = tyVal₂) :
                                                                                                                                                                                                                          interp tyVal₁ ncwf₁ interp tyVal₂ ncwf₂
                                                                                                                                                                                                                          def Auto.Embedding.Lam.NatConst.interp_equiv {n : NatConst} {s : LamSort} (tyVal : NatType u) (ncwf : n.LamWF s) :
                                                                                                                                                                                                                          LamWF.interp tyVal ncwf interp tyVal n
                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                          • =
                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                              def Auto.Embedding.Lam.IntConst.LamWF.interp {i : IntConst} {s : LamSort} (tyVal : NatType u) (lwf : i.LamWF s) :
                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                theorem Auto.Embedding.Lam.IntConst.LamWF.interp_lvalIrrelevance {i₁ : IntConst} {s₁ : LamSort} {i₂ : IntConst} {s₂ : LamSort} (tyVal₁ tyVal₂ : NatType u) (icwf₁ : i₁.LamWF s₁) (icwf₂ : i₂.LamWF s₂) (HBeq : i₁ = i₂) (hTyVal : tyVal₁ = tyVal₂) :
                                                                                                                                                                                                                                interp tyVal₁ icwf₁ interp tyVal₂ icwf₂
                                                                                                                                                                                                                                def Auto.Embedding.Lam.IntConst.interp_equiv {i : IntConst} {s : LamSort} (tyVal : NatType u) (icwf : i.LamWF s) :
                                                                                                                                                                                                                                LamWF.interp tyVal icwf interp tyVal i
                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                • =
                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.StringConst.LamWF.interp_lvalIrrelevance {sc₁ : StringConst} {s₁ : LamSort} {sc₂ : StringConst} {s₂ : LamSort} (tyVal₁ tyVal₂ : NatType u) (scwf₁ : sc₁.LamWF s₁) (scwf₂ : sc₂.LamWF s₂) (HBeq : sc₁ = sc₂) (hTyVal : tyVal₁ = tyVal₂) :
                                                                                                                                                                                                                                  interp tyVal₁ scwf₁ interp tyVal₂ scwf₂
                                                                                                                                                                                                                                  def Auto.Embedding.Lam.StringConst.interp_equiv {sc : StringConst} {s : LamSort} (tyVal : NatType u) (scwf : sc.LamWF s) :
                                                                                                                                                                                                                                  LamWF.interp tyVal scwf interp tyVal sc
                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                  • =
                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                      def Auto.Embedding.Lam.BitVecConst.LamWF.interp {b : BitVecConst} {s : LamSort} (tyVal : NatType u) (lwf : b.LamWF s) :
                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                        theorem Auto.Embedding.Lam.BitVecConst.LamWF.interp_lvalIrrelevance {b₁ : BitVecConst} {s₁ : LamSort} {b₂ : BitVecConst} {s₂ : LamSort} (tyVal₁ tyVal₂ : NatType u) (bcwf₁ : b₁.LamWF s₁) (bcwf₂ : b₂.LamWF s₂) (HBeq : b₁ = b₂) (hTyVal : tyVal₁ = tyVal₂) :
                                                                                                                                                                                                                                        interp tyVal₁ bcwf₁ interp tyVal₂ bcwf₂
                                                                                                                                                                                                                                        def Auto.Embedding.Lam.BitVecConst.interp_equiv {b : BitVecConst} {s : LamSort} (tyVal : NatType u) (bcwf : b.LamWF s) :
                                                                                                                                                                                                                                        LamWF.interp tyVal bcwf interp tyVal b
                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                        • =
                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                              theorem Auto.Embedding.Lam.LamBaseTerm.LamWF.interp_heq {b₁ : LamBaseTerm} {s₁ : LamSort} {b₂ : LamBaseTerm} {s₂ : LamSort} (lval : LamValuation) (lwf₁ : LamWF lval.toLamTyVal b₁ s₁) (lwf₂ : LamWF lval.toLamTyVal b₂ s₂) (HBeq : b₁ = b₂) :
                                                                                                                                                                                                                                              interp lval lwf₁ interp lval lwf₂
                                                                                                                                                                                                                                              theorem Auto.Embedding.Lam.LamBaseTerm.LamWF.interp_lvalIrrelevance {b₁ : LamBaseTerm} {s₁ : LamSort} {b₂ : LamBaseTerm} {s₂ : LamSort} (lval₁ lval₂ : LamValuation) (lwf₁ : LamWF lval₁.toLamTyVal b₁ s₁) (lwf₂ : LamWF lval₂.toLamTyVal b₂ s₂) (HBeq : b₁ = b₂) (hTyVal : lval₁.tyVal = lval₂.tyVal) (hLamILTy : lval₁.lamILTy = lval₂.lamILTy) (hILVal : lval₁.ilVal lval₂.ilVal) :
                                                                                                                                                                                                                                              interp lval₁ lwf₁ interp lval₂ lwf₂
                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                              • =
                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamTyVal.insertEVarAt_eVarIrrelevance {n pos : Nat} {ty : LamSort} {ltv₁ : LamTyVal} (H : n < pos) :
                                                                                                                                                                                                                                                  let ltv₂ := { lamVarTy := ltv₁.lamVarTy, lamILTy := ltv₁.lamILTy, lamEVarTy := replaceAt ty pos ltv₁.lamEVarTy }; ltv₁.lamEVarTy n = ltv₂.lamEVarTy n
                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamValuation.insertEVarAt_eVarIrrelevance {n pos : Nat} {ty : LamSort} {lval₁ : LamValuation} {val : LamSort.interp lval₁.tyVal ty} (H : n < pos) :
                                                                                                                                                                                                                                                  let lval₂ := lval₁.insertEVarAt ty val pos; lval₁.lamEVarTy n = lval₂.lamEVarTy n lval₁.eVarVal n lval₂.eVarVal n
                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                    def Auto.Embedding.Lam.LamTerm.flip (argTy₁ argTy₂ resTy : LamSort) :
                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                      theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_flip {argTy₁ argTy₂ resTy : LamSort} :
                                                                                                                                                                                                                                                      (flip argTy₁ argTy₂ resTy).maxEVarSucc = 0
                                                                                                                                                                                                                                                      def Auto.Embedding.Lam.LamTerm.flipApp (t : LamTerm) (argTy₁ argTy₂ resTy : LamSort) :
                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                        theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_flipApp {t : LamTerm} {argTy₁ argTy₂ resTy : LamSort} :
                                                                                                                                                                                                                                                        (t.flipApp argTy₁ argTy₂ resTy).maxEVarSucc = t.maxEVarSucc
                                                                                                                                                                                                                                                        @[reducible, inline]
                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                            @[reducible, inline]
                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                    @[reducible, inline]
                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                        @[reducible, inline]
                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                            @[reducible, inline]
                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                  @[reducible, inline]
                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                    @[reducible, inline]
                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                      @[reducible, inline]
                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                        @[reducible, inline]
                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                          @[reducible, inline]
                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                            @[reducible, inline]
                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                              @[reducible, inline]
                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                @[reducible, inline]
                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                        Instances For

                                                                                                                                                                                                                                                                                                                          Make BitVec.ofNat n i

                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                          Instances For

                                                                                                                                                                                                                                                                                                                            Make BitVec.ofInt n i

                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                    theorem Auto.Embedding.Lam.LamTerm.maxEVarSucc_mkAppN {args : List (LamSort × LamTerm)} {n : Nat} {t : LamTerm} (hs : HList (fun (x : LamSort × LamTerm) => match x with | (fst, arg) => arg.maxEVarSucc n) args) (ht : t.maxEVarSucc n) :
                                                                                                                                                                                                                                                                                                                                    theorem Auto.Embedding.Lam.LamTerm.mkLamFN_append {t : LamTerm} {l₁ l₂ : List LamSort} :
                                                                                                                                                                                                                                                                                                                                    t.mkLamFN (l₁ ++ l₂) = (t.mkLamFN l₂).mkLamFN l₁

                                                                                                                                                                                                                                                                                                                                    Given λ (_ : ty₀) ⋯ (_ : tyᵢ₋₁), body, return body

                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                    Instances For

                                                                                                                                                                                                                                                                                                                                      Given λ (_ : ty₀) ⋯ (_ : tyᵢ₋₁), _, return [ty₀, ⋯, tyᵢ₋₁]

                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                          theorem Auto.Embedding.Lam.LamTerm.getLamTysN_getLamBodyN_eq {n : Nat} {t : LamTerm} {l : List LamSort} {body : LamTerm} (hTys : getLamTysN n t = some l) (hBody : getLamBodyN n t = some body) :
                                                                                                                                                                                                                                                                                                                                          t = body.mkLamFN l
                                                                                                                                                                                                                                                                                                                                          @[irreducible]
                                                                                                                                                                                                                                                                                                                                          noncomputable def Auto.Embedding.Lam.LamTerm.maxEVarSucc_getAppArgsAux {args : List (LamSort × LamTerm)} {n : Nat} {t : LamTerm} (hs : HList (fun (x : LamSort × LamTerm) => match x with | (fst, arg) => arg.maxEVarSucc n) args) (ht : t.maxEVarSucc n) :
                                                                                                                                                                                                                                                                                                                                          HList (fun (x : LamSort × LamTerm) => match x with | (fst, arg) => arg.maxEVarSucc n) (getAppArgsAux args t)
                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                            @[irreducible]
                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamTerm.maxEVarSucc_getAppArgsNAux {args : List (LamSort × LamTerm)} {m n : Nat} {t : LamTerm} {args' : List (LamSort × LamTerm)} (hs : HList (fun (x : LamSort × LamTerm) => match x with | (fst, arg) => arg.maxEVarSucc m) args) (ht : t.maxEVarSucc m) (heq : getAppArgsNAux n args t = some args') :
                                                                                                                                                                                                                                                                                                                                            HList (fun (x : LamSort × LamTerm) => match x with | (fst, arg) => arg.maxEVarSucc m) args'
                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                              theorem Auto.Embedding.Lam.LamTerm.getAppArgsN_succ_app {n : Nat} {s : LamSort} {fn arg : LamTerm} :
                                                                                                                                                                                                                                                                                                                                              getAppArgsN n.succ (app s fn arg) = (getAppArgsN n fn).bind fun (x : List (LamSort × LamTerm)) => some (x ++ [(s, arg)])
                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                • t.getForallEFBody = t
                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                      theorem Auto.Embedding.Lam.LamTerm.eq_of_beq_eq_true {t₁ t₂ : LamTerm} :
                                                                                                                                                                                                                                                                                                                                                      t₁.beq t₂ = truet₁ = t₂

                                                                                                                                                                                                                                                                                                                                                      LamTerm.containsSort has a nice property : · Let s be a non-function type. If a term t satisfies LamWF ltv ⟨lctx, t, s'⟩, and s occurs in neither t nor s', then for all atoms occurring in t, s does not occur in the atom's type. To see this, notice that the argument type is recorded in .app, and the binder type is recorded in .lam

                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                        theorem Auto.Embedding.Lam.LamTerm.lamCheck?_irrelevence {ltv : LamTyVal} {lctx₁ lctx₂ : NatLamSort} {t : LamTerm} (hirr : ∀ (n : Nat), n < t.maxLooseBVarSucclctx₁ n = lctx₂ n) :
                                                                                                                                                                                                                                                                                                                                                        lamCheck? ltv lctx₁ t = lamCheck? ltv lctx₂ t

                                                                                                                                                                                                                                                                                                                                                        Judgement. lamVarTy, lctx ⊢ term : type? We put rterm before rty to avoid dependent elimination failure

                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamWF.unique {lctx : NatLamSort} {t : LamTerm} {s₁ s₂ : LamSort} {ltv : LamTyVal} (lwf₁ : LamWF ltv { lctx := lctx, rterm := t, rty := s₁ }) (lwf₂ : LamWF ltv { lctx := lctx, rterm := t, rty := s₂ }) :
                                                                                                                                                                                                                                                                                                                                                            s₁ = s₂ lwf₁ lwf₂
                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                            • =
                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.insertEVarAt_eIdx {s : LamSort} {eIdx : Nat} {lamEVarTy' lctx : NatLamSort} {ltv : LamTyVal} :
                                                                                                                                                                                                                                                                                                                                                              LamWF { lamVarTy := ltv.lamVarTy, lamILTy := ltv.lamILTy, lamEVarTy := replaceAt s eIdx lamEVarTy' } { lctx := lctx, rterm := LamTerm.etom eIdx, rty := s }
                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                def Auto.Embedding.Lam.LamWF.eVarIrrelevance {ltv₁ : LamTyVal} {lctx : NatLamSort} {t : LamTerm} {s : LamSort} {ltv₂ : LamTyVal} (hLamVarTy : ltv₁.lamVarTy = ltv₂.lamVarTy) (hLamILTy : ltv₁.lamILTy = ltv₂.lamILTy) (hirr : ∀ (n : Nat), n < t.maxEVarSuccltv₁.lamEVarTy n = ltv₂.lamEVarTy n) (lwf : LamWF ltv₁ { lctx := lctx, rterm := t, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                LamWF ltv₂ { lctx := lctx, rterm := t, rty := s }
                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                  def Auto.Embedding.Lam.LamWF.getAtom {lctx : NatLamSort} {n : Nat} {s : LamSort} {ltv : LamTyVal} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.atom n, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                  ltv.lamVarTy n = s
                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                  • =
                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                    def Auto.Embedding.Lam.LamWF.getEtom {lctx : NatLamSort} {n : Nat} {s : LamSort} {ltv : LamTyVal} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.etom n, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                    ltv.lamEVarTy n = s
                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                    • =
                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                      def Auto.Embedding.Lam.LamWF.getBase {lctx : NatLamSort} {b : LamBaseTerm} {s : LamSort} {ltv : LamTyVal} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.base b, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                        def Auto.Embedding.Lam.LamWF.getBVar {lctx : NatLamSort} {n : Nat} {s : LamSort} {ltv : LamTyVal} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.bvar n, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                        lctx n = s
                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                        • =
                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                          def Auto.Embedding.Lam.LamWF.getLam {lctx : NatLamSort} {s : LamSort} {body : LamTerm} {argTy : LamSort} {ltv : LamTyVal} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.lam s body, rty := s.func argTy }) :
                                                                                                                                                                                                                                                                                                                                                                          LamWF ltv { lctx := pushLCtx s lctx, rterm := body, rty := argTy }
                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamWF.getFn {lctx : NatLamSort} {argTy : LamSort} {fn arg : LamTerm} {resTy : LamSort} {ltv : LamTyVal} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.app argTy fn arg, rty := resTy }) :
                                                                                                                                                                                                                                                                                                                                                                            LamWF ltv { lctx := lctx, rterm := fn, rty := argTy.func resTy }
                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.getArg {lctx : NatLamSort} {argTy : LamSort} {fn arg : LamTerm} {resTy : LamSort} {ltv : LamTyVal} (wft : LamWF ltv { lctx := lctx, rterm := LamTerm.app argTy fn arg, rty := resTy }) :
                                                                                                                                                                                                                                                                                                                                                                              LamWF ltv { lctx := lctx, rterm := arg, rty := argTy }
                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                def Auto.Embedding.Lam.LamWF.flip {ltv : LamTyVal} {lctx : NatLamSort} {argTy₁ argTy₂ resTy : LamSort} :
                                                                                                                                                                                                                                                                                                                                                                                LamWF ltv { lctx := lctx, rterm := LamTerm.flip argTy₁ argTy₂ resTy, rty := (argTy₁.func (argTy₂.func resTy)).func (argTy₂.func (argTy₁.func resTy)) }
                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                  def Auto.Embedding.Lam.LamWF.flipApp {ltv : LamTyVal} {lctx : NatLamSort} {t : LamTerm} {argTy₁ argTy₂ resTy : LamSort} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := argTy₁.func (argTy₂.func resTy) }) :
                                                                                                                                                                                                                                                                                                                                                                                  LamWF ltv { lctx := lctx, rterm := t.flipApp argTy₁ argTy₂ resTy, rty := argTy₂.func (argTy₁.func resTy) }
                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.mkAnd {lctx : NatLamSort} {t₁ t₂ : LamTerm} {ltv : LamTyVal} (wft₁ : LamWF ltv { lctx := lctx, rterm := t₁, rty := LamSort.base LamBaseSort.prop }) (wft₂ : LamWF ltv { lctx := lctx, rterm := t₂, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                              LamWF ltv { lctx := lctx, rterm := t₁.mkAnd t₂, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                def Auto.Embedding.Lam.LamWF.mkOr {lctx : NatLamSort} {t₁ t₂ : LamTerm} {ltv : LamTyVal} (wft₁ : LamWF ltv { lctx := lctx, rterm := t₁, rty := LamSort.base LamBaseSort.prop }) (wft₂ : LamWF ltv { lctx := lctx, rterm := t₂, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                LamWF ltv { lctx := lctx, rterm := t₁.mkOr t₂, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                  def Auto.Embedding.Lam.LamWF.mkImp {lctx : NatLamSort} {t₁ t₂ : LamTerm} {ltv : LamTyVal} (wft₁ : LamWF ltv { lctx := lctx, rterm := t₁, rty := LamSort.base LamBaseSort.prop }) (wft₂ : LamWF ltv { lctx := lctx, rterm := t₂, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                  LamWF ltv { lctx := lctx, rterm := t₁.mkImp t₂, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                    def Auto.Embedding.Lam.LamWF.mkIff {lctx : NatLamSort} {t₁ t₂ : LamTerm} {ltv : LamTyVal} (wft₁ : LamWF ltv { lctx := lctx, rterm := t₁, rty := LamSort.base LamBaseSort.prop }) (wft₂ : LamWF ltv { lctx := lctx, rterm := t₂, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                    LamWF ltv { lctx := lctx, rterm := t₁.mkIff t₂, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                      def Auto.Embedding.Lam.LamWF.mkEq {lctx : NatLamSort} {t₁ : LamTerm} {s : LamSort} {t₂ : LamTerm} {ltv : LamTyVal} (wft₁ : LamWF ltv { lctx := lctx, rterm := t₁, rty := s }) (wft₂ : LamWF ltv { lctx := lctx, rterm := t₂, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                                                      LamWF ltv { lctx := lctx, rterm := LamTerm.mkEq s t₁ t₂, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                        theorem Auto.Embedding.Lam.LamWF.mkEq_sortEq {ltv : LamTyVal} {lctx : NatLamSort} {s' s'' s : LamSort} {t₁ t₂ : LamTerm} {rty : LamSort} (hwf : LamWF ltv { lctx := lctx, rterm := LamTerm.app s' (LamTerm.app s'' (LamTerm.base (LamBaseTerm.eq s)) t₁) t₂, rty := rty }) :
                                                                                                                                                                                                                                                                                                                                                                                                        def Auto.Embedding.Lam.LamWF.mkForallE {lctx : NatLamSort} {p : LamTerm} {s : LamSort} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := lctx, rterm := p, rty := s.func (LamSort.base LamBaseSort.prop) }) :
                                                                                                                                                                                                                                                                                                                                                                                                        LamWF ltv { lctx := lctx, rterm := LamTerm.mkForallE s p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                          def Auto.Embedding.Lam.LamWF.mkForallEF {s : LamSort} {lctx : NatLamSort} {p : LamTerm} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := pushLCtx s lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                          LamWF ltv { lctx := lctx, rterm := LamTerm.mkForallEF s p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamWF.fromMkForallEF {lctx : NatLamSort} {s : LamSort} {p : LamTerm} {ltv : LamTyVal} (wf : LamWF ltv { lctx := lctx, rterm := LamTerm.mkForallEF s p, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                            LamWF ltv { lctx := pushLCtx s lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.mkExistE {lctx : NatLamSort} {p : LamTerm} {s : LamSort} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := lctx, rterm := p, rty := s.func (LamSort.base LamBaseSort.prop) }) :
                                                                                                                                                                                                                                                                                                                                                                                                              LamWF ltv { lctx := lctx, rterm := LamTerm.mkExistE s p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                def Auto.Embedding.Lam.LamWF.mkExistEF {s : LamSort} {lctx : NatLamSort} {p : LamTerm} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := pushLCtx s lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                                LamWF ltv { lctx := lctx, rterm := LamTerm.mkExistEF s p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                  def Auto.Embedding.Lam.LamWF.fromMkExistEF {lctx : NatLamSort} {s : LamSort} {p : LamTerm} {ltv : LamTyVal} (wf : LamWF ltv { lctx := lctx, rterm := LamTerm.mkExistEF s p, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                                  LamWF ltv { lctx := pushLCtx s lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                    def Auto.Embedding.Lam.LamWF.mkIte {lctx : NatLamSort} {p x : LamTerm} {s : LamSort} {y : LamTerm} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }) (wfx : LamWF ltv { lctx := lctx, rterm := x, rty := s }) (wfy : LamWF ltv { lctx := lctx, rterm := y, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                                                                    LamWF ltv { lctx := lctx, rterm := LamTerm.mkIte s p x y, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                      def Auto.Embedding.Lam.LamWF.mkNatBinOp {binOp : NatConst} {s : LamSort} {lctx : NatLamSort} {a b : LamTerm} {ltv : LamTyVal} (wfop : binOp.LamWF ((LamSort.base LamBaseSort.nat).func ((LamSort.base LamBaseSort.nat).func s))) (wfa : LamWF ltv { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.nat }) (wfb : LamWF ltv { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) :
                                                                                                                                                                                                                                                                                                                                                                                                                      LamWF ltv { lctx := lctx, rterm := LamTerm.mkNatBinOp binOp a b, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                        def Auto.Embedding.Lam.LamWF.mkIOfNat {lctx : NatLamSort} {n : LamTerm} {ltv : LamTyVal} (wfn : LamWF ltv { lctx := lctx, rterm := n, rty := LamSort.base LamBaseSort.nat }) :
                                                                                                                                                                                                                                                                                                                                                                                                                        LamWF ltv { lctx := lctx, rterm := n.mkIOfNat, rty := LamSort.base LamBaseSort.int }
                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                          def Auto.Embedding.Lam.LamWF.mkINegSucc {lctx : NatLamSort} {n : LamTerm} {ltv : LamTyVal} (wfn : LamWF ltv { lctx := lctx, rterm := n, rty := LamSort.base LamBaseSort.nat }) :
                                                                                                                                                                                                                                                                                                                                                                                                                          LamWF ltv { lctx := lctx, rterm := n.mkINegSucc, rty := LamSort.base LamBaseSort.int }
                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamWF.mkIntUOp {uop : IntConst} {s : LamSort} {lctx : NatLamSort} {a : LamTerm} {ltv : LamTyVal} (wfop : uop.LamWF ((LamSort.base LamBaseSort.int).func s)) (wfa : LamWF ltv { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.int }) :
                                                                                                                                                                                                                                                                                                                                                                                                                            LamWF ltv { lctx := lctx, rterm := LamTerm.mkIntUOp uop a, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.mkIntBinOp {binOp : IntConst} {s : LamSort} {lctx : NatLamSort} {a b : LamTerm} {ltv : LamTyVal} (wfop : binOp.LamWF ((LamSort.base LamBaseSort.int).func ((LamSort.base LamBaseSort.int).func s))) (wfa : LamWF ltv { lctx := lctx, rterm := a, rty := LamSort.base LamBaseSort.int }) (wfb : LamWF ltv { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.int }) :
                                                                                                                                                                                                                                                                                                                                                                                                                              LamWF ltv { lctx := lctx, rterm := LamTerm.mkIntBinOp binOp a b, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                def Auto.Embedding.Lam.LamWF.mkBvofNat {lctx : NatLamSort} {i : LamTerm} {n : Nat} {ltv : LamTyVal} (wfi : LamWF ltv { lctx := lctx, rterm := i, rty := LamSort.base LamBaseSort.nat }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                LamWF ltv { lctx := lctx, rterm := LamTerm.mkBvofNat n i, rty := LamSort.base (LamBaseSort.bv n) }
                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                  def Auto.Embedding.Lam.LamWF.mkBvofInt {lctx : NatLamSort} {i : LamTerm} {n : Nat} {ltv : LamTyVal} (wfi : LamWF ltv { lctx := lctx, rterm := i, rty := LamSort.base LamBaseSort.int }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                  LamWF ltv { lctx := lctx, rterm := LamTerm.mkBvofInt n i, rty := LamSort.base (LamBaseSort.bv n) }
                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                    def Auto.Embedding.Lam.LamWF.mkBvUOp {uop : BitVecConst} {n : Nat} {s : LamSort} {lctx : NatLamSort} {a : LamTerm} {ltv : LamTyVal} (wfop : uop.LamWF ((LamSort.base (LamBaseSort.bv n)).func s)) (wfa : LamWF ltv { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                    LamWF ltv { lctx := lctx, rterm := LamTerm.mkBvUOp n uop a, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                      def Auto.Embedding.Lam.LamWF.mkBvBinOp {binOp : BitVecConst} {n : Nat} {s : LamSort} {lctx : NatLamSort} {a b : LamTerm} {ltv : LamTyVal} (wfop : binOp.LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base (LamBaseSort.bv n)).func s))) (wfa : LamWF ltv { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF ltv { lctx := lctx, rterm := b, rty := LamSort.base (LamBaseSort.bv n) }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                      LamWF ltv { lctx := lctx, rterm := LamTerm.mkBvBinOp n binOp a b, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                        def Auto.Embedding.Lam.LamWF.mkBvNatBinOp {binOp : BitVecConst} {n : Nat} {s : LamSort} {lctx : NatLamSort} {a b : LamTerm} {ltv : LamTyVal} (wfop : binOp.LamWF ((LamSort.base (LamBaseSort.bv n)).func ((LamSort.base LamBaseSort.nat).func s))) (wfa : LamWF ltv { lctx := lctx, rterm := a, rty := LamSort.base (LamBaseSort.bv n) }) (wfb : LamWF ltv { lctx := lctx, rterm := b, rty := LamSort.base LamBaseSort.nat }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                        LamWF ltv { lctx := lctx, rterm := LamTerm.mkBvNatBinOp n binOp a b, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                          def Auto.Embedding.Lam.LamWF.mkAppN {ltv : LamTyVal} {lctx : NatLamSort} {f : LamTerm} {args : List (LamSort × LamTerm)} {s : LamSort} (wfFn : LamWF ltv { lctx := lctx, rterm := f, rty := s.mkFuncs (List.map Prod.fst args) }) (wfArgs : HList (fun (x : LamSort × LamTerm) => match x with | (s, t) => LamWF ltv { lctx := lctx, rterm := t, rty := s }) args) :
                                                                                                                                                                                                                                                                                                                                                                                                                                          LamWF ltv { lctx := lctx, rterm := f.mkAppN args, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamWF.fnWFOfMkAppN {ltv : LamTyVal} {lctx : NatLamSort} {s : LamSort} {f : LamTerm} {args : List (LamSort × LamTerm)} (wfApp : LamWF ltv { lctx := lctx, rterm := f.mkAppN args, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                            LamWF ltv { lctx := lctx, rterm := f, rty := s.mkFuncs (List.map Prod.fst args) }
                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.argsWFOfMkAppN {ltv : LamTyVal} {lctx : NatLamSort} {args : List (LamSort × LamTerm)} {s : LamSort} {f : LamTerm} (wfApp : LamWF ltv { lctx := lctx, rterm := f.mkAppN args, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                              HList (fun (x : LamSort × LamTerm) => match x with | (s, t) => LamWF ltv { lctx := lctx, rterm := t, rty := s }) args
                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                def Auto.Embedding.Lam.LamWF.mkLamFN {lctx : NatLamSort} {p : LamTerm} {s : LamSort} {ls : List LamSort} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := pushLCtxs ls.reverse lctx, rterm := p, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                LamWF ltv { lctx := lctx, rterm := p.mkLamFN ls, rty := s.mkFuncs ls }
                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                  def Auto.Embedding.Lam.LamWF.fromMkLamFN {lctx : NatLamSort} {p : LamTerm} {ls : List LamSort} {s : LamSort} {ltv : LamTyVal} (wfLam : LamWF ltv { lctx := lctx, rterm := p.mkLamFN ls, rty := s.mkFuncs ls }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                  LamWF ltv { lctx := pushLCtxs ls.reverse lctx, rterm := p, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                    def Auto.Embedding.Lam.LamWF.fromMkLamFN_s_eq_mkFuncs_reverse {lctx : NatLamSort} {p : LamTerm} {ls : List LamSort} {s : LamSort} {ltv : LamTyVal} (wfLam : LamWF ltv { lctx := lctx, rterm := p.mkLamFN ls, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                    (s' : LamSort) ×' s = s'.mkFuncs ls
                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                      def Auto.Embedding.Lam.LamWF.mkForallEFN {lctx : NatLamSort} {p : LamTerm} {ls : List LamSort} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := pushLCtxs ls.reverse lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                      LamWF ltv { lctx := lctx, rterm := p.mkForallEFN ls, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                        def Auto.Embedding.Lam.LamWF.fromMkForallEFN {lctx : NatLamSort} {p : LamTerm} {ls : List LamSort} {ltv : LamTyVal} (wf : LamWF ltv { lctx := lctx, rterm := p.mkForallEFN ls, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                        LamWF ltv { lctx := pushLCtxs ls.reverse lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                          def Auto.Embedding.Lam.LamWF.mkForallEFN' {ls : List LamSort} {lctx : NatLamSort} {p : LamTerm} {ltv : LamTyVal} (wfp : LamWF ltv { lctx := pushLCtxs ls lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                          LamWF ltv { lctx := lctx, rterm := p.mkForallEFN ls.reverse, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamWF.fromMkForallEFN' {lctx : NatLamSort} {p : LamTerm} {ls : List LamSort} {ltv : LamTyVal} (wf : LamWF ltv { lctx := lctx, rterm := p.mkForallEFN ls.reverse, rty := LamSort.base LamBaseSort.prop }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                            LamWF ltv { lctx := pushLCtxs ls lctx, rterm := p, rty := LamSort.base LamBaseSort.prop }
                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.ofAtom' {ltv : LamTyVal} {lctx : NatLamSort} (n : Nat) (s : LamSort) (heq : ltv.lamVarTy n = s) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                              LamWF ltv { lctx := lctx, rterm := LamTerm.atom n, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                def Auto.Embedding.Lam.LamWF.ofEtom' {ltv : LamTyVal} {lctx : NatLamSort} (n : Nat) (s : LamSort) (heq : ltv.lamEVarTy n = s) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                LamWF ltv { lctx := lctx, rterm := LamTerm.etom n, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  def Auto.Embedding.Lam.LamWF.ofBVar' {ltv : LamTyVal} {lctx : NatLamSort} (n : Nat) (s : LamSort) (heq : lctx n = s) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  LamWF ltv { lctx := lctx, rterm := LamTerm.bvar n, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                  Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    def Auto.Embedding.Lam.LamWF.bvarApps {ltv : LamTyVal} {ex lctx : List LamSort} {lctx' : NatLamSort} {t : LamTerm} {s : LamSort} (wft : LamWF ltv { lctx := pushLCtxs (ex.reverseAux lctx) lctx', rterm := t, rty := s.mkFuncsRev lctx }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    LamWF ltv { lctx := pushLCtxs (ex.reverseAux lctx) lctx', rterm := t.bvarApps lctx ex.length, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      def Auto.Embedding.Lam.LamWF.bvarAppsRev {ltv : LamTyVal} {lctx' : NatLamSort} {t : LamTerm} {s : LamSort} {lctx : List LamSort} (wft : LamWF ltv { lctx := pushLCtxs lctx.reverse lctx', rterm := t, rty := s.mkFuncs lctx }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      LamWF ltv { lctx := pushLCtxs lctx.reverse lctx', rterm := t.bvarAppsRev lctx, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      • wft_2.bvarAppsRev = wft_2
                                                                                                                                                                                                                                                                                                                                                                                                                                                                      Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        def Auto.Embedding.Lam.LamWF.fromBVarAppsRev {ltv : LamTyVal} {lctx' : NatLamSort} {s : LamSort} {t : LamTerm} {lctx : List LamSort} (wfAp : LamWF ltv { lctx := pushLCtxs lctx.reverse lctx', rterm := t.bvarAppsRev lctx, rty := s }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        LamWF ltv { lctx := pushLCtxs lctx.reverse lctx', rterm := t, rty := s.mkFuncs lctx }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        • wfAp_2.fromBVarAppsRev = wfAp_2
                                                                                                                                                                                                                                                                                                                                                                                                                                                                        Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          • =
                                                                                                                                                                                                                                                                                                                                                                                                                                                                          Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            def Auto.Embedding.Lam.LamTerm.lamCheck?_of_lamWF {ltv : LamTyVal} {lctx : NatLamSort} {t : LamTerm} {ty : LamSort} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            ∀ (a : LamWF ltv { lctx := lctx, rterm := t, rty := ty }), lamCheck? ltv lctx t = some ty
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            • =
                                                                                                                                                                                                                                                                                                                                                                                                                                                                            Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              @[irreducible]
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              def Auto.Embedding.Lam.LamWF.ofNonemptyLamWF {ltv : LamTyVal} {lctx : NatLamSort} {t : LamTerm} {s : LamSort} (H : Nonempty (LamWF ltv { lctx := lctx, rterm := t, rty := s })) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              LamWF ltv { lctx := lctx, rterm := t, rty := s }
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                                                                                                                                                                                                                                                                                              Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                noncomputable def Auto.Embedding.Lam.LamWF.interp {t : LamTerm} {rty : LamSort} (lval : LamValuation) (lctxTy : NatLamSort) (lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)) (lwf : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t, rty := rty }) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Equations
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                Instances For
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_eq {lctxTy : NatLamSort} {t₁ : LamTerm} {rty : LamSort} {t₂ : LamTerm} (lval : LamValuation) {lctxTerm₁ lctxTerm₂ : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} (HLCtxTermEq : lctxTerm₁ lctxTerm₂) (lwf₁ : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t₁, rty := rty }) (lwf₂ : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t₂, rty := rty }) (HTeq : t₁ = t₂) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm₁ lwf₁ = interp lval lctxTy lctxTerm₂ lwf₂
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_heq {t₁ : LamTerm} {rty₁ : LamSort} {t₂ : LamTerm} {rty₂ : LamSort} (lval : LamValuation) {lctxTy₁ lctxTy₂ : NatLamSort} (HLCtxTyEq : lctxTy₁ = lctxTy₂) {lctxTerm₁ : (n : Nat) → LamSort.interp lval.tyVal (lctxTy₁ n)} {lctxTerm₂ : (n : Nat) → LamSort.interp lval.tyVal (lctxTy₂ n)} (HLCtxTermEq : lctxTerm₁ lctxTerm₂) (lwf₁ : LamWF lval.toLamTyVal { lctx := lctxTy₁, rterm := t₁, rty := rty₁ }) (lwf₂ : LamWF lval.toLamTyVal { lctx := lctxTy₂, rterm := t₂, rty := rty₂ }) (HTeq : t₁ = t₂) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy₁ lctxTerm₁ lwf₁ interp lval lctxTy₂ lctxTerm₂ lwf₂
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_substLCtxTerm {lctxTy : NatLamSort} {t : LamTerm} {s : LamSort} {lctxTy' : NatLamSort} {lval : LamValuation} {wf : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t, rty := s }} {wf' : LamWF lval.toLamTyVal { lctx := lctxTy', rterm := t, rty := s }} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} {lctxTerm' : (n : Nat) → LamSort.interp lval.tyVal (lctxTy' n)} (HLCtxTyEq : lctxTy = lctxTy') (HLCtxTermEq : lctxTerm lctxTerm') :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wf = interp lval lctxTy' lctxTerm' wf'
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_substLCtxTerm_rec {lctxTy : NatLamSort} {t : LamTerm} {s : LamSort} {lctxTy' : NatLamSort} {lval : LamValuation} {wf : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t, rty := s }} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} {lctxTerm' : (n : Nat) → LamSort.interp lval.tyVal (lctxTy' n)} (HLCtxTyEq : lctxTy = lctxTy') (HLCtxTermEq : lctxTerm lctxTerm') :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wf = interp lval lctxTy' lctxTerm' (HLCtxTyEq wf)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_substWF {lctxTy : NatLamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} {wf wf' : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := t, rty := s }} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wf = interp lval lctxTy lctxTerm wf'
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_prop_eqExists {lctx : NatLamSort} {t : LamTerm} {lval : LamValuation} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} {wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  ( (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }), (interp lval lctx lctxTerm wf).down) = (interp lval lctx lctxTerm wf).down
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_prop_eqForall {lctx : NatLamSort} {t : LamTerm} {lval : LamValuation} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} {wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (∀ (wf : LamWF lval.toLamTyVal { lctx := lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }), (interp lval lctx lctxTerm wf).down) = (interp lval lctx lctxTerm wf).down
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_atom {lctxTy : NatLamSort} {n : Nat} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.atom n, rty := s }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wft lval.varVal n
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_etom {lctxTy : NatLamSort} {n : Nat} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.etom n, rty := s }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wft lval.eVarVal n
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_base {lctxTy : NatLamSort} {b : LamBaseTerm} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.base b, rty := s }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wft = LamBaseTerm.LamWF.interp lval wft.getBase
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_base' {lctxTy : NatLamSort} {b : LamBaseTerm} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.base b, rty := s }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wft LamBaseTerm.interp lval b
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_bvar {lctxTy : NatLamSort} {n : Nat} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.bvar n, rty := s }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wft lctxTerm n
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_lam {lctxTy : NatLamSort} {argTy : LamSort} {body : LamTerm} {resTy : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.lam argTy body, rty := argTy.func resTy }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wft = fun (x : LamSort.interp lval.tyVal argTy) => interp lval (pushLCtx argTy lctxTy) (pushLCtxDep x lctxTerm) wft.getLam
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_app {lctxTy : NatLamSort} {argTy : LamSort} {fn arg : LamTerm} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := lctxTy, rterm := LamTerm.app argTy fn arg, rty := s }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy lctxTerm wft = interp lval lctxTy lctxTerm wft.getFn (interp lval lctxTy lctxTerm wft.getArg)
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_bvarAppsRev {lctxTy' : NatLamSort} {t : LamTerm} {s : LamSort} {lctxTy : List LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := pushLCtxs lctxTy.reverse lctxTy', rterm := t, rty := s.mkFuncs lctxTy }) (wfAp : LamWF lval.toLamTyVal { lctx := pushLCtxs lctxTy.reverse lctxTy', rterm := t.bvarAppsRev lctxTy, rty := s }) {valPre : HList (LamSort.interp lval.tyVal) lctxTyLamSort.interp lval.tyVal s} {lctxTerm : HList (LamSort.interp lval.tyVal) lctxTy} {lctxTerm' : (n : Nat) → LamSort.interp lval.tyVal (lctxTy' n)} (ht : interp lval (pushLCtxs lctxTy.reverse lctxTy') (pushLCtxsDep lctxTerm.reverse lctxTerm') wft LamSort.curry valPre) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval (pushLCtxs lctxTy.reverse lctxTy') (pushLCtxsDep lctxTerm.reverse lctxTerm') wfAp valPre lctxTerm
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_eqForallEF {s : LamSort} {lctx : NatLamSort} {t : LamTerm} {lval : LamValuation} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} {wf : LamWF lval.toLamTyVal { lctx := pushLCtx s lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (interp lval lctx lctxTerm wf.mkForallEF).down = ∀ (x : LamSort.interp lval.tyVal s), (interp lval (pushLCtx s lctx) (pushLCtxDep x lctxTerm) wf).down
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_eqForallEFN' {lctx : NatLamSort} {ls : List LamSort} {t : LamTerm} {lval : LamValuation} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} {wf : LamWF lval.toLamTyVal { lctx := pushLCtxs ls lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (interp lval lctx lctxTerm wf.mkForallEFN').down = ∀ (xs : HList (LamSort.interp lval.tyVal) ls), (interp lval (pushLCtxs ls lctx) (pushLCtxsDep xs lctxTerm) wf).down
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_eqForallEFN {lctx : NatLamSort} {t : LamTerm} {lval : LamValuation} {ls : List LamSort} {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctx n)} {wf : LamWF lval.toLamTyVal { lctx := pushLCtxs ls.reverse lctx, rterm := t, rty := LamSort.base LamBaseSort.prop }} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  (interp lval lctx lctxTerm wf.mkForallEFN).down = ∀ (xs : HList (LamSort.interp lval.tyVal) ls.reverse), (interp lval (pushLCtxs ls.reverse lctx) (pushLCtxsDep xs lctxTerm) wf).down
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_bvarApps {tyex lctx : List LamSort} {lctx' : NatLamSort} {t : LamTerm} {s : LamSort} {lval : LamValuation} (wft : LamWF lval.toLamTyVal { lctx := pushLCtxs (tyex.reverseAux lctx) lctx', rterm := t, rty := s.mkFuncsRev lctx }) (wfAp : LamWF lval.toLamTyVal { lctx := pushLCtxs (tyex.reverseAux lctx) lctx', rterm := t.bvarApps lctx tyex.length, rty := s }) {valPre : HList (LamSort.interp lval.tyVal) lctxLamSort.interp lval.tyVal s} {termex : HList (LamSort.interp lval.tyVal) tyex} {lctxTerm : HList (LamSort.interp lval.tyVal) lctx} {lctxTerm' : (n : Nat) → LamSort.interp lval.tyVal (lctx' n)} (ht : interp lval (pushLCtxs (tyex.reverseAux lctx) lctx') (pushLCtxsDep (termex.reverseAux lctxTerm) lctxTerm') wft LamSort.curryRev valPre) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval (pushLCtxs (tyex.reverseAux lctx) lctx') (pushLCtxsDep (termex.reverseAux lctxTerm) lctxTerm') wfAp valPre lctxTerm
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_insertEVarAt_eIdx {ty : LamSort} {pos : Nat} {lamEVarTy' lctxTy : NatLamSort} {rty : LamSort} {lval : LamValuation} {val : LamSort.interp lval.tyVal ty} (lwf : LamWF (let __src := lval.toLamTyVal; { lamVarTy := __src.lamVarTy, lamILTy := __src.lamILTy, lamEVarTy := replaceAt ty pos lamEVarTy' }) { lctx := lctxTy, rterm := LamTerm.etom pos, rty := rty }) {lctxTerm : (n : Nat) → LamSort.interp lval.tyVal (lctxTy n)} {eVarVal' : (n : Nat) → LamSort.interp lval.tyVal (lamEVarTy' n)} :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  let lval' := { lamVarTy := lval.lamVarTy, lamILTy := lval.lamILTy, lamEVarTy := replaceAt ty pos lamEVarTy', tyVal := lval.tyVal, varVal := lval.varVal, ilVal := lval.ilVal, eVarVal := replaceAtDep val pos eVarVal' }; interp lval' lctxTy lctxTerm lwf val
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_eVarIrrelevance (lval₁ lval₂ : LamValuation) {lctxTy₁ lctxTy₂ : NatLamSort} {lctxTerm₁ : (n : Nat) → LamSort.interp lval₁.tyVal (lctxTy₁ n)} {lctxTerm₂ : (n : Nat) → LamSort.interp lval₂.tyVal (lctxTy₂ n)} {t : LamTerm} {rty : LamSort} (lwf₁ : LamWF lval₁.toLamTyVal { lctx := lctxTy₁, rterm := t, rty := rty }) (lwf₂ : LamWF lval₂.toLamTyVal { lctx := lctxTy₂, rterm := t, rty := rty }) (hLamVarTy : lval₁.lamVarTy = lval₂.lamVarTy) (hLamILTy : lval₁.lamILTy = lval₂.lamILTy) (hTyVal : lval₁.tyVal lval₂.tyVal) (hVarVal : lval₁.varVal lval₂.varVal) (hILVal : lval₁.ilVal lval₂.ilVal) (hLCtxTy : lctxTy₁ = lctxTy₂) (hLCtxTerm : lctxTerm₁ lctxTerm₂) (hirr : ∀ (n : Nat), n < t.maxEVarSucclval₁.lamEVarTy n = lval₂.lamEVarTy n lval₁.eVarVal n lval₂.eVarVal n) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval₁ lctxTy₁ lctxTerm₁ lwf₁ interp lval₂ lctxTy₂ lctxTerm₂ lwf₂
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamWF.interp_lctxIrrelevance (lval : LamValuation) {lctxTy₁ lctxTy₂ : NatLamSort} {lctxTerm₁ : (n : Nat) → LamSort.interp lval.tyVal (lctxTy₁ n)} {lctxTerm₂ : (n : Nat) → LamSort.interp lval.tyVal (lctxTy₂ n)} {t : LamTerm} {rty : LamSort} (lwf₁ : LamWF lval.toLamTyVal { lctx := lctxTy₁, rterm := t, rty := rty }) (lwf₂ : LamWF lval.toLamTyVal { lctx := lctxTy₂, rterm := t, rty := rty }) (hirr : ∀ (n : Nat), n < t.maxLooseBVarSucclctxTy₁ n = lctxTy₂ n lctxTerm₁ n lctxTerm₂ n) :
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  interp lval lctxTy₁ lctxTerm₁ lwf₁ interp lval lctxTy₂ lctxTerm₂ lwf₂
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                  theorem Auto.Embedding.Lam.LamTerm.forallEFBody_forallEFTys_eq {ltv : LamTyVal} {lctx : NatLamSort} {t : LamTerm} {s : LamSort} (wft : LamWF ltv { lctx := lctx, rterm := t, rty := s }) :