Theorems · Theorem · logic and foundations

List.reverseRec.hcongr_5

∀ (α α' : Type u_1),
  α = α' →
    ∀ (motive : List α → Sort u_2) (motive' : List α' → Sort u_2),
      motive ≍ motive' →
        ∀ (nil : motive []) (nil' : motive' []),
          nil ≍ nil' →
            ∀ (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a]))
              (append_singleton' : (l : List α') → (a : α') → motive' l → motive' (l ++ [a])),
              append_singleton ≍ append_singleton' →
                ∀ (l : List α) (l' : List α'),
                  l ≍ l' → List.reverseRec nil append_singleton l ≍ List.reverseRec nil' append_singleton' l'

Defined in

Mathlib.Data.List.Induction

Cited by

0 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext