In this short, code-heavy post, we extend some of the work from a previous post to reason about the cardinalities of sums and products.

Last time we saw how to reason about the cardinalities of sets using the `Fin` type. The main technical tool was a axiomless replacement for dependent destruction. This time we’ll prove a slightly more interesting result about the cardinality of a particular inductive type.

First we pull in the definition of `Fin`, and, just like last time, we define cardinality in terms of a bijection to `Fin.t n`.

``````    Require Import Fin.

Definition cardinality (A : Type) (n : nat) : Prop :=
exists (to_fin    : A -> Fin.t n)
(from_fin  : Fin.t n -> A),
(forall x, from_fin (to_fin x) = x) /\
(forall y, to_fin (from_fin y) = y).
``````

The goal of the post will be to prove a result about the cardinality of the type `T`, given below.

``````    Inductive T (A : Type) : Type :=
| T1 : T A
| T2 : A -> T A
| T3 : A -> A -> T A.
``````

There is an obvious relationship between the cardinality of `A` and the cardinality of `T A`.

``````    Theorem cardinality_T :
forall A n,
cardinality A n ->
cardinality (T A) (1 + n + n * n).
``````

Our strategy will be to prove lemmas about the cardinalities of sums and products. We’ll then express `T` as a sum of products and apply our lemmas.

``````    Lemma card_bij :
forall A B (f : A -> B) g n,
(forall x, f (g x) = x) ->
(forall x, g (f x) = x) ->
cardinality A n ->
cardinality B n.
Proof.

\$(function () {
\$("#context-0").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>B</span>) (<span style='color:#a0522d'>g</span> : <span style='color:#a0522d'>B</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>A</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, f (g x) = x) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, g (f x) = x) -> cardinality A n -> cardinality B n\n\n<hr />\n  <span style='color:#00008b'>unfold</span> cardinality.\n\n<hr />\n  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>B</span>) (<span style='color:#a0522d'>g</span> : <span style='color:#a0522d'>B</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>A</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, f (g x) = x) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, g (f x) = x) ->\n   (<span style='color:#00008b'>exists</span> (to_fin : A -> t n) (from_fin : t n -> A),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, from_fin (to_fin x) = x) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)) ->\n   <span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold cardinality.

\$(function () {
\$("#context-1").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>B</span>) (<span style='color:#a0522d'>g</span> : <span style='color:#a0522d'>B</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>A</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, f (g x) = x) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, g (f x) = x) ->\n   (<span style='color:#00008b'>exists</span> (to_fin : A -> t n) (from_fin : t n -> A),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, from_fin (to_fin x) = x) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)) ->\n   <span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)\n\n<hr />\n  <span style='color:#00008b'>firstorder</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f : A -> B\n  g : B -> A\n  n : nat\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, f (g x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, g (f x) = x\n  x : A -> t n\n  x0 : t n -> A\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>A</span>, x0 (x x1) = x1\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x (x0 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x1) = x1) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
firstorder.

\$(function () {
\$("#context-2").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f : A -> B\n  g : B -> A\n  n : nat\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, f (g x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, g (f x) = x\n  x : A -> t n\n  x0 : t n -> A\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>A</span>, x0 (x x1) = x1\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x (x0 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x1) = x1) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)\n\n<hr />\n  <span style='color:#00008b'>exists</span> (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>z</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>x</span> (<span style='color:#a0522d'>g</span> <span style='color:#a0522d'>z</span>)), (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>z</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>f</span> (<span style='color:#a0522d'>x0</span> <span style='color:#a0522d'>z</span>)).\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f : A -> B\n  g : B -> A\n  n : nat\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, f (g x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, g (f x) = x\n  x : A -> t n\n  x0 : t n -> A\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>A</span>, x0 (x x1) = x1\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x (x0 y) = y\n  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>B</span>, f (x0 (x (g x1))) = x1) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x (g (f (x0 y))) = y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
exists (fun z => x (g z)), (fun z => f (x0 z)).

\$(function () {
\$("#context-3").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f : A -> B\n  g : B -> A\n  n : nat\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, f (g x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, g (f x) = x\n  x : A -> t n\n  x0 : t n -> A\n  H11 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>A</span>, x0 (x x1) = x1\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x (x0 y) = y\n  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x1</span> : <span style='color:#a0522d'>B</span>, f (x0 (x (g x1))) = x1) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x (g (f (x0 y))) = y)\n\n<hr />\n  <span style='color:#00008b'>intuition</span> <span style='color:#ff0000'>congruence</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
intuition congruence.
Qed.
``````

We then define conversion functions between `T` and an encoding in terms of sum and product types…

``````
Definition T_to_sum {A : Type} (x : T A) : (unit + A) + A * A :=
match x with
| T1 => inl (inl tt)
| T2 a => inl (inr a)
| T3 a b => inr (a,b)
end.

Definition sum_to_T {A : Type} (x : (unit + A) + A * A) : T A :=
match x with
| inl l => match l with
| inl _ => T1 A
| inr a => T2 A a
end
| inr (a,b) => T3 A a b
end.
``````

…and prove the conversions are inverses.

``````    Lemma to_from_T :
forall A (x : T A),
sum_to_T (T_to_sum x) = x.
Proof.

\$(function () {
\$("#context-4").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>T</span> <span style='color:#a0522d'>A</span>), sum_to_T (T_to_sum x) = x\n\n<hr />\n  <span style='color:#00008b'>destruct</span> x; <span style='color:#00008b'>auto</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
destruct x; auto.
Qed.

Require Import JRWTactics.

Lemma from_to_T :
forall A (x : unit + A + A * A),
T_to_sum (sum_to_T x) = x.
Proof.

\$(function () {
\$("#context-5").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>unit</span> + <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>A</span>), T_to_sum (sum_to_T x) = x\n\n<hr />\n  <span style='color:#00008b'>intros</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  ============================\n   T_to_sum (sum_to_T x) = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
intros.

\$(function () {
\$("#context-6").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  ============================\n   T_to_sum (sum_to_T x) = x\n\n<hr />\n  <span style='color:#00008b'>unfold</span> T_to_sum, sum_to_T.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  ============================\n   <span style='color:#228b22'>match</span>\n     <span style='color:#228b22'>match</span> x <span style='color:#228b22'>with</span>\n     | inl (inl _) => T1 A\n     | inl (inr a) => T2 A a\n     | inr (a, b) => T3 A a b\n     <span style='color:#228b22'>end</span>\n   <span style='color:#228b22'>with</span>\n   | T1 => inl (inl tt)\n   | T2 a => inl (inr a)\n   | T3 a b => inr (a, b)\n   <span style='color:#228b22'>end</span> = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold T_to_sum, sum_to_T.

\$(function () {
\$("#context-7").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  ============================\n   <span style='color:#228b22'>match</span>\n     <span style='color:#228b22'>match</span> x <span style='color:#228b22'>with</span>\n     | inl (inl _) => T1 A\n     | inl (inr a) => T2 A a\n     | inr (a, b) => T3 A a b\n     <span style='color:#228b22'>end</span>\n   <span style='color:#228b22'>with</span>\n   | T1 => inl (inl tt)\n   | T2 a => inl (inr a)\n   | T3 a b => inr (a, b)\n   <span style='color:#228b22'>end</span> = x\n\n<hr />\n  <span style='color:#a020f0'>repeat</span> break_match; <span style='color:#00008b'>auto</span>; <span style='color:#a020f0'>try</span> <span style='color:#ff0000'>congruence</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  s : unit + A\n  u : unit\n  Heqs0 : s = inl u\n  Heqs : x = inl (inl u)\n  Heqt : T1 A = T1 A\n  ============================\n   inl (inl tt) = inl (inl u)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
repeat break_match; auto; try congruence.

\$(function () {
\$("#context-8").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  s : unit + A\n  u : unit\n  Heqs0 : s = inl u\n  Heqs : x = inl (inl u)\n  Heqt : T1 A = T1 A\n  ============================\n   inl (inl tt) = inl (inl u)\n\n<hr />\n  <span style='color:#00008b'>destruct</span> u. <span style='color:#00008b'>auto</span>.\n  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  s : unit + A\n  Heqs0 : s = inl tt\n  Heqs : x = inl (inl tt)\n  Heqt : T1 A = T1 A\n  ============================\n   inl (inl tt) = inl (inl tt)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
destruct u.

\$(function () {
\$("#context-9").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  x : unit + A + A * A\n  s : unit + A\n  Heqs0 : s = inl tt\n  Heqs : x = inl (inl tt)\n  Heqt : T1 A = T1 A\n  ============================\n   inl (inl tt) = inl (inl tt)\n\n<hr />\n  <span style='color:#00008b'>auto</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto.
Qed.
``````

The only trick with the second proof is that we use the custom tactic `break_match` which finds a `match` statement in the context and calls `destruct` on its discriminee. You can get my tactic library on GitHub.

Using this bijection and the lemma above, we can prove that the cardinality of `T A` is the same as the cardinality of `unit + A + A * A`.

``````    Lemma card_T_sum_prod :
forall A n,
cardinality (unit + A + A * A) n ->
cardinality (T A) n.
Proof.

\$(function () {
\$("#context-10").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   cardinality (unit + A + A * A) n -> cardinality (T A) n\n\n<hr />\n  <span style='color:#00008b'>eauto</span> <span style='color:#228b22'>using</span> card_bij, to_from_T, from_to_T.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
eauto using card_bij, to_from_T, from_to_T.
Qed.
``````

With this lemma in our back pocket, all that’s left is to analyze the cardinality of `unit + A + A * A`. We’ll prove lemmas about the cardinality of `unit`, sums, and products, and then put them all together in the final theorem.

We start by showing that `unit` has cardinality 1.

``````    Lemma card_unit :
cardinality unit 1.
Proof.

\$(function () {
\$("#context-11").tooltip({
content: "<pre><code>  y : t 1\n  ============================\n   F1 = y\n\n<hr />\n  <span style='color:#00008b'>unfold</span> cardinality.\n\n<hr />\n  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : unit -> t 1) (from_fin : t 1 -> unit),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>unit</span>, from_fin (to_fin x) = x) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>1</span>, to_fin (from_fin y) = y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold cardinality.

\$(function () {
\$("#context-12").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : unit -> t 1) (from_fin : t 1 -> unit),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>unit</span>, from_fin (to_fin x) = x) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>1</span>, to_fin (from_fin y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>exists</span> (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>F1</span>), (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>tt</span>).\n\n<hr />\n  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>unit</span>, tt = x) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>1</span>, F1 = y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
exists (fun _ => F1), (fun _ => tt).

\$(function () {
\$("#context-13").tooltip({
content: "<pre><code>  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>unit</span>, tt = x) /\\ (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>1</span>, F1 = y)\n\n\n<hr />\n  <span style='color:#00008b'>intuition</span>.\n\n<hr />\n  x : unit\n  ============================\n   tt = x\n\nsubgoal 2 (ID 493) is:\n F1 = y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
intuition.

\$(function () {
\$("#context-14").tooltip({
content: "<pre><code>  x : unit\n  ============================\n   tt = x\n\n<hr />\n  <span style='color:#00008b'>destruct</span> x. <span style='color:#00008b'>auto</span>.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- destruct x. auto.

\$(function () {
\$("#context-15").tooltip({
content: "<pre><code>  y : t 1\n  ============================\n   F1 = y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- (* hover here to see subgoal *)
``````

Here we want to do case analysis on `y` to prove that it must be `F1`. For this we’ll need some of the dependent case analysis work from last time. `fin_case` implements a “destruction principle” for `Fin.t`. It also now comes with a new and improved proof: Look Ma, no decidable equality!

``````    Definition fin_case n x :
forall (P : Fin.t (S n) -> Type),
P F1 ->
(forall y, P (FS y)) ->
P x :=
match x as x0 in Fin.t n0
return
forall P,
match n0 as n0' return (t n0' -> (t n0' -> Type) -> Type) with
| 0 => fun _ _ => False
| S m => fun x P => P F1 -> (forall x0, P (FS x0)) -> P x
end x0 P
with
| F1 _ => fun _ H1 _ => H1
| FS _ _ => fun _ _ HS => HS _
end.
``````

We wrap up `fin_case` in a tactic that makes it easy to case analysis on a variable.

``````    Ltac fin_dep_destruct v :=
pattern v; apply fin_case; clear v; intros.
``````

We can now finish the proof about the cardinality of `unit` using our new `fin_dep_destruct` tactic, as well as `solve_by_inversion` which searches for a contradiction in the context (in this case, an inhabitant of `Fin.t 0`).

``````
\$(function () {
\$("#context-16").tooltip({
content: "<pre><code>  y : t 1\n  ============================\n   F1 = y\n\n<hr />\n   fin_dep_destruct y.\n\n<hr />\n  ============================\n   F1 = F1\n\nsubgoal 2  F1 = FS y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
fin_dep_destruct y.

\$(function () {
\$("#context-17").tooltip({
content: "<pre><code>  ============================\n   F1 = F1\n\n<hr />\n  + <span style='color:#00008b'>auto</span>.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ auto.

\$(function () {
\$("#context-18").tooltip({
content: "<pre><code>  y : t 0\n  ============================\n   F1 = FS y\n\n<hr />\n  + solve_by_inversion.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ solve_by_inversion.
Qed.
``````

We now prove that the cardinality of a sum of types is the sum of the cardinalities. (Say that 5 times fast.) We first define a conversion function from `A + B` to `Fin.t (n + m)` given conversions from `A` to `Fin.t n` and `B` to `Fin.t m`.

``````    Definition from_sum {n m A B} (f : A -> Fin.t n) (g : B -> Fin.t m)
(x : A + B) : Fin.t (n + m) :=
match x with
| inl a => L _ (f a)
| inr b => R _ (g b)
end.
``````

This was easy to define because of the built in functions `L` and `R`, which inject `Fin.t n` and `Fin.t m` into `Fin.t (n + m)`, respectively.

To go the other direction, we first define a sort of inverse of `L` and `R`, which, given a `Fin.t (n + m)`, returns either a `Fin.t n` or a `Fin.t m`.

``````    Fixpoint fin_of_sum_to_sum_of_fin {n m} {struct n} :
Fin.t (n + m) -> Fin.t n + Fin.t m :=
match n as n' return Fin.t (n' + m) -> Fin.t n' + Fin.t m with
| 0 => fun x : t m => inr x
| S n' => fun x : t (S (n' + m)) =>
fin_case _ x _
(inl F1)
(fun x' : t (n' + m) =>
match fin_of_sum_to_sum_of_fin x' with
| inl a => inl (FS a)
| inr b => inr b
end)
end.
``````

Here we use `fin_case` as a programming construct, in contrast to our previous use in proofs. Our fancy new “proof” (ie, implementation) of `fin_case` will make reasoning about this function possible. The key property of `fin_of_sum_to_sum_of_fin` is that it correctly distinguishes elements in the range of `L` from those in the range of `R`. We show these two properties next.

``````    Lemma fin_of_sum_to_sum_of_fin_L :
forall m (x : Fin.t m) n,
fin_of_sum_to_sum_of_fin (L n x) = inl x.
Proof.

\$(function () {
\$("#context-19").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   fin_of_sum_to_sum_of_fin (L n x) = inl x\n\n\n<hr />\n  <span style='color:#00008b'>induction</span> m; <span style='color:#00008b'>intros</span>; <span style='color:#00008b'>simpl</span> <span style='color:#228b22'>in</span> *.\n\n<hr />\n  x : t 0\n  n : nat\n  ============================\n   inr (L n x) = inl x\n\nsubgoal 2 (ID 620) is:\n fin_case (m + n) (L n x) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>m</span>) + <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)<span style='color:#a0522d'>%type</span>)\n   (inl F1)\n   (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span>\n    <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n    | inl a => inl (FS a)\n    | inr b => inr b\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
induction m; intros; simpl in *.

\$(function () {
\$("#context-20").tooltip({
content: "<pre><code>  x : t 0\n  n : nat\n  ============================\n   inr (L n x) = inl x\n\n<hr />\n  - solve_by_inversion.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- solve_by_inversion.

\$(function () {
\$("#context-21").tooltip({
content: "<pre><code>  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  x : t (S m)\n  n : nat\n  ============================\n   fin_case (m + n) (L n x) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>m</span>) + <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inl x\n\n<hr />\n  fin_dep_destruct x.\n\n<hr />\n  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  n : nat\n  ============================\n   fin_case (m + n) (L n F1) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>m</span>) + <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inl F1\n\nsubgoal 2 (ID 665) is:\n fin_case (m + n) (L n (FS y))\n   (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>m</span>) + <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)<span style='color:#a0522d'>%type</span>)\n   (inl F1)\n   (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span>\n    <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n    | inl a => inl (FS a)\n    <span style='color:#228b22'>end</span>) = inl (FS y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- fin_dep_destruct x.

\$(function () {
\$("#context-22").tooltip({
content: "<pre><code>  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  n : nat\n  ============================\n   fin_case (m + n) (L n F1) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>m</span>) + <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inl F1\n\n<hr />\n    <span style='color:#00008b'>auto</span>.\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ auto.

\$(function () {
\$("#context-23").tooltip({
content: "<pre><code>  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  n : nat\n  y : t m\n  ============================\n   fin_case (m + n) (L n (FS y))\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>m</span>) + <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inl (FS y)\n\n<hr />\n    <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  n : nat\n  y : t m\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (L n y) <span style='color:#228b22'>with</span>\n   | inl a => inl (FS a)\n   | inr b => inr b\n   <span style='color:#228b22'>end</span> = inl (FS y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ simpl.

\$(function () {
\$("#context-24").tooltip({
content: "<pre><code>  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  n : nat\n  y : t m\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (L n y) <span style='color:#228b22'>with</span>\n   | inl a => inl (FS a)\n   | inr b => inr b\n   <span style='color:#228b22'>end</span> = inl (FS y)\n\n<hr />\n      find_higher_order_rewrite.\n\n<hr />\n  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  n : nat\n  y : t m\n  ============================\n   inl (FS y) = inl (FS y)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_higher_order_rewrite.

\$(function () {
\$("#context-25").tooltip({
content: "<pre><code>  m : nat\n  IHm : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>), fin_of_sum_to_sum_of_fin (L n x) = inl x\n  n : nat\n  y : t m\n  ============================\n   inl (FS y) = inl (FS y)\n\n<hr />\n      <span style='color:#00008b'>auto</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto.
Qed.

Lemma fin_of_sum_to_sum_of_fin_R :
forall n m (x : Fin.t m),
fin_of_sum_to_sum_of_fin (R n x) = inr x.
Proof.

\$(function () {
\$("#context-26").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>), fin_of_sum_to_sum_of_fin (R n x) = inr x\n\n\n<hr />\n  <span style='color:#00008b'>induction</span> n; <span style='color:#00008b'>intros</span>; <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  m : nat\n  x : t m\n  ============================\n   inr x = inr x\n\nsubgoal 2 (ID 693) is:\n <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (R n x) <span style='color:#228b22'>with</span>\n | inl a => inl (FS a)\n | inr b => inr b\n <span style='color:#228b22'>end</span> = inr x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
induction n; intros; simpl.

\$(function () {
\$("#context-27").tooltip({
content: "<pre><code>  m : nat\n  x : t m\n  ============================\n   inr x = inr x\n\n<hr />\n  - <span style='color:#00008b'>auto</span>.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- auto.

\$(function () {
\$("#context-28").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>), fin_of_sum_to_sum_of_fin (R n x) = inr x\n  m : nat\n  x : t m\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (R n x) <span style='color:#228b22'>with</span>\n   | inl a => inl (FS a)\n   | inr b => inr b\n   <span style='color:#228b22'>end</span> = inr x\n\n<hr />\n  find_higher_order_rewrite.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>), fin_of_sum_to_sum_of_fin (R n x) = inr x\n  m : nat\n  x : t m\n  ============================\n   inr x = inr x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- find_higher_order_rewrite.

\$(function () {
\$("#context-29").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>), fin_of_sum_to_sum_of_fin (R n x) = inr x\n  m : nat\n  x : t m\n  ============================\n   inr x = inr x\n\n<hr />\n    <span style='color:#00008b'>auto</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto.
Qed.
``````

We used another custom tactic here, `find_higher_order_rewrite`, which searches the context for a universally quantified equality, and tries to rewrite with it everywhere without introducing any new subgoals. This avoids dependence on automatically generated hypothesis names. In all cases it is possible to replace a call to `find_higher_order_rewrite` with a call to `rewrite` by passing in the correct name. Other than this new tactic, the proofs are easy.

With `fin_of_sum_to_sum_of_fin` defined, we can now define the inverse of `from_sum`.

``````    Definition to_sum {n m A B} (f : Fin.t n -> A) (g : Fin.t m -> B)
(x : Fin.t (n + m)) : A + B :=
match fin_of_sum_to_sum_of_fin x with
| inl a => inl (f a)
| inr b => inr (g b)
end.
``````

And we can prove that the two are inverses. In the first direction, we show that encoding an element of `A + B` into an element of `Fin.t (n + m)` and then decoding it returns the same element. We’ll need to use our lemmas that relate `fin_of_sum_to_sum_of_fin` to `L` and `R`.

``````    Lemma to_from_sum :
forall n m A B f1 f2 g1 g2 x,
(forall x, f2 (f1 x) = x) ->
(forall x, g2 (g1 x) = x) ->
@to_sum n m A B f2 g2 (from_sum f1 g1 x) = x.
Proof.

\$(function () {
\$("#context-30").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f1</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)\n     (f2 : t n -> A) (g1 : B -> t m) (g2 : t m -> B)\n     (x : A + B),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x0) = x0) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x0) = x0) -> to_sum f2 g2 (from_sum f1 g1 x) = x\n\n<hr />\n  <span style='color:#00008b'>unfold</span> to_sum.\n\n<hr />\n  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f1</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)\n     (f2 : t n -> A) (g1 : B -> t m) (g2 : t m -> B)\n     (x : A + B),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x0) = x0) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x0) = x0) ->\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (from_sum f1 g1 x) <span style='color:#228b22'>with</span>\n   | inl a => inl (f2 a)\n   | inr b => inr (g2 b)\n   <span style='color:#228b22'>end</span> = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold to_sum.

\$(function () {
\$("#context-31").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f1</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)\n     (f2 : t n -> A) (g1 : B -> t m) (g2 : t m -> B)\n     (x : A + B),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x0) = x0) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x0) = x0) ->\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (from_sum f1 g1 x) <span style='color:#228b22'>with</span>\n   | inl a => inl (f2 a)\n   | inr b => inr (g2 b)\n   <span style='color:#228b22'>end</span> = x\n\n<hr />\n  <span style='color:#00008b'>intros</span>.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A + B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x0) = x0\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (from_sum f1 g1 x) <span style='color:#228b22'>with</span>\n   | inl a => inl (f2 a)\n   | inr b => inr (g2 b)\n   <span style='color:#228b22'>end</span> = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
intros.

\$(function () {
\$("#context-32").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A + B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x0) = x0\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (from_sum f1 g1 x) <span style='color:#228b22'>with</span>\n   | inl a => inl (f2 a)\n   | inr b => inr (g2 b)\n   <span style='color:#228b22'>end</span> = x\n\n<hr />\n  <span style='color:#00008b'>destruct</span> x; <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  a : A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x) = x\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (L m (f1 a)) <span style='color:#228b22'>with</span>\n   | inl a0 => inl (f2 a0)\n   | inr b => inr (g2 b)\n   <span style='color:#228b22'>end</span> = inl a\n\nsubgoal 2 (ID 765) is:\n <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (R n (g1 b)) <span style='color:#228b22'>with</span>\n | inl a => inl (f2 a)\n | inr b0 => inr (g2 b0)\n <span style='color:#228b22'>end</span> = inr b\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
destruct x; simpl.

\$(function () {
\$("#context-33").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  a : A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x) = x\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (L m (f1 a)) <span style='color:#228b22'>with</span>\n   | inl a0 => inl (f2 a0)\n   | inr b => inr (g2 b)\n   <span style='color:#228b22'>end</span> = inl a\n\n<hr />\n  <span style='color:#00008b'>rewrite</span> fin_of_sum_to_sum_of_fin_L.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  a : A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x) = x\n  ============================\n   inl (f2 (f1 a)) = inl a\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- rewrite fin_of_sum_to_sum_of_fin_L.

\$(function () {
\$("#context-34").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  a : A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x) = x\n  ============================\n   inl (f2 (f1 a)) = inl a\n\n<hr />\n    <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> f_equal.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using f_equal.

\$(function () {
\$("#context-35").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  b : B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x) = x\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (R n (g1 b)) <span style='color:#228b22'>with</span>\n   | inl a => inl (f2 a)\n   | inr b0 => inr (g2 b0)\n   <span style='color:#228b22'>end</span> = inr b\n\n<hr />\n  - <span style='color:#00008b'>rewrite</span> fin_of_sum_to_sum_of_fin_R.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  b : B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x) = x\n  ============================\n   inr (g2 (g1 b)) = inr b\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- rewrite fin_of_sum_to_sum_of_fin_R.

\$(function () {
\$("#context-36").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  b : B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, f2 (f1 x) = x\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, g2 (g1 x) = x\n  ============================\n   inr (g2 (g1 b)) = inr b\n\n<hr />\n    <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> f_equal.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using f_equal.
Qed.
``````

In the other direction, we follow the structure of `to_sum`, doing case analysis on the result of `fin_of_sum_to_sum_of_fin`.

``````    Lemma from_to_sum :
forall n m A B f1 f2 g1 g2 x,
(forall x, f1 (f2 x) = x) ->
(forall x, g1 (g2 x) = x) ->
from_sum f1 g1 (@to_sum n m A B f2 g2 x) = x.
Proof.

\$(function () {
\$("#context-37").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f1</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)\n     (f2 : t n -> A) (g1 : B -> t m) (g2 : t m -> B)\n     (x : t (n + m)),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0) -> from_sum f1 g1 (to_sum f2 g2 x) = x\n\n<hr />\n  <span style='color:#00008b'>intros</span>.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  ============================\n   from_sum f1 g1 (to_sum f2 g2 x) = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
intros.

\$(function () {
\$("#context-38").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  ============================\n   from_sum f1 g1 (to_sum f2 g2 x) = x\n\n<hr />\n  <span style='color:#00008b'>unfold</span> to_sum.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  ============================\n   from_sum f1 g1\n     <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x <span style='color:#228b22'>with</span>\n     | inl a => inl (f2 a)\n     | inr b => inr (g2 b)\n     <span style='color:#228b22'>end</span> = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold to_sum.

\$(function () {
\$("#context-39").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  ============================\n   from_sum f1 g1\n     <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x <span style='color:#228b22'>with</span>\n     | inl a => inl (f2 a)\n     | inr b => inr (g2 b)\n     <span style='color:#228b22'>end</span> = x\n\n\n<hr />\n  break_match; <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  t : t n\n  Heqs : fin_of_sum_to_sum_of_fin x = inl t\n  ============================\n   L m (f1 (f2 t)) = x\n\nsubgoal 2 (ID 838) is:\n  R n (g1 (g2 t)) = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
break_match; simpl.

\$(function () {
\$("#context-40").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  t : t n\n  Heqs : fin_of_sum_to_sum_of_fin x = inl t\n  ============================\n   L m (f1 (f2 t)) = x\n\n<hr />\n  find_higher_order_rewrite.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  t : t n\n  Heqs : fin_of_sum_to_sum_of_fin x = inl t\n  ============================\n   L m t = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- find_higher_order_rewrite.
``````

To continue, we need a lemma that says that if `fin_of_sum_to_sum_of_fin` returns an element in the “left side”, then its argument must have been in the range of `L`. This is sort of the converse of `fin_of_sum_to_sum_of_fin_L`.

``````    Lemma L_fin_of_sum_to_sum_of_fin :
forall n m (x : Fin.t (n + m)) t,
fin_of_sum_to_sum_of_fin x = inl t ->
L m t = x.
Proof.

\$(function () {
\$("#context-41").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n   fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n\n\n<hr />\n  <span style='color:#00008b'>induction</span> n; <span style='color:#00008b'>intros</span>.\n\n<hr />\n  m : nat\n  x : t (0 + m)\n  t : t 0\n  H : fin_of_sum_to_sum_of_fin x = inl t\n  ============================\n   L m t = x\n\nsubgoal 2 (ID 865) is:\n L m t = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
induction n; intros.

\$(function () {
\$("#context-42").tooltip({
content: "<pre><code>  m : nat\n  x : t (0 + m)\n  t : t 0\n  H : fin_of_sum_to_sum_of_fin x = inl t\n  ============================\n   L m t = x\n\n<hr />\n  solve_by_inversion.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- solve_by_inversion.

\$(function () {
\$("#context-43").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  x : t (S n + m)\n  t : t (S n)\n  H : fin_of_sum_to_sum_of_fin x = inl t\n  ============================\n   L m t = x\n\n<hr />\n  <span style='color:#00008b'>simpl</span> <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  x : t (S (n + m))\n  t : t (S n)\n  H : fin_case (n + m) x\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inl t\n  ============================\n   L m t = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- simpl in *.

\$(function () {
\$("#context-44").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  x : t (S (n + m))\n  t : t (S n)\n  H : fin_case (n + m) x\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inl t\n  ============================\n   L m t = x\n\n<hr />\n    <span style='color:#00008b'>revert</span> H.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  x : t (S (n + m))\n  t : t (S n)\n  ============================\n   fin_case (n + m) x\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inl t -> L m t = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
revert H.

\$(function () {
\$("#context-45").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  x : t (S (n + m))\n  t : t (S n)\n  ============================\n   fin_case (n + m) x\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inl t -> L m t = x\n\n<hr />\n    fin_dep_destruct x.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  H : fin_case (n + m) F1\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inl t\n  ============================\n   L m t = F1\n\nsubgoal 2 (ID 896) is:\n L m t = FS y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
fin_dep_destruct x.

\$(function () {
\$("#context-46").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  H : fin_case (n + m) F1\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inl t\n  ============================\n   L m t = F1\n\n<hr />\n    solve_by_inversion.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ solve_by_inversion.

\$(function () {
\$("#context-47").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  y : Fin.t (n + m)\n  H : fin_case (n + m) (FS y)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inl t\n  ============================\n   L m t = FS y\n\n<hr />\n    + <span style='color:#00008b'>simpl</span> <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  y : Fin.t (n + m)\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin y <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span> = inl t\n  ============================\n   L m t = FS y\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ simpl in *.

\$(function () {
\$("#context-48").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  y : Fin.t (n + m)\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin y <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span> = inl t\n  ============================\n   L m t = FS y\n\n<hr />\n      break_match.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  y : Fin.t (n + m)\n  t0 : Fin.t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  H : inl (FS t0) = inl t\n  ============================\n   L m t = FS y\n\nsubgoal 2 (ID 945) is:\n L m t = FS y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
break_match.

\$(function () {
\$("#context-49").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  y : Fin.t (n + m)\n  t0 : Fin.t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  H : inl (FS t0) = inl t\n  ============================\n   L m t = FS y\n\n<hr />\n      * find_inversion.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  y : t (n + m)\n  t0 : t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  ============================\n   L m (FS t0) = FS y\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
* find_inversion.

\$(function () {
\$("#context-50").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  y : t (n + m)\n  t0 : t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  ============================\n   L m (FS t0) = FS y\n\n<hr />\n        <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  y : t (n + m)\n  t0 : t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  ============================\n   FS (L m t0) = FS y\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
simpl.

\$(function () {
\$("#context-51").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  y : t (n + m)\n  t0 : t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  ============================\n   FS (L m t0) = FS y\n\n<hr />\n        <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> f_equal.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using f_equal.

\$(function () {
\$("#context-52").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>),\n        fin_of_sum_to_sum_of_fin x = inl t -> L m t = x\n  m : nat\n  t : t (S n)\n  y : Fin.t (n + m)\n  t0 : Fin.t m\n  Heqs : fin_of_sum_to_sum_of_fin y = inr t0\n  H : inr t0 = inl t\n  ============================\n   L m t = FS y\n\n<hr />\n      <span style='color:#ff0000'>discriminate</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
* discriminate.
Qed.
``````

Here’s yet another custom tactic, `find_inversion`, which searches the context for an equality to invert on. In this case, we have a hypothesis of the form `inl x = inl y`. Inverting this yields the equality `x = y`. Again, the purpose of this tactic is solely to eliminate dependence on hypothesis names. One could just as easily call `inversion` directly.

We can now finish the first subcase of the second direction.

``````
\$(function () {
\$("#context-53").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  t : t n\n  Heqs : fin_of_sum_to_sum_of_fin x = inl t\n  ============================\n   L m t = x\n\n<hr />\n    <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> L_fin_of_sum_to_sum_of_fin.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using L_fin_of_sum_to_sum_of_fin.
``````

The second case starts out the same way

``````
\$(function () {
\$("#context-54").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  t : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  ============================\n   R n (g1 (g2 t)) = x\n\n<hr />\n  find_higher_order_rewrite.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  t : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  ============================\n   R n t = x\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- find_higher_order_rewrite.
``````

To proceed, we’ll need an analogous result about `R`.

``````    Lemma R_fin_of_sum_to_sum_of_fin :
forall n m (x : Fin.t (n + m)) t,
fin_of_sum_to_sum_of_fin x = inr t ->
R n t = x.
Proof.

\$(function () {
\$("#context-55").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n   fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n\n\n<hr />\n  <span style='color:#00008b'>induction</span> n; <span style='color:#00008b'>intros</span>; <span style='color:#00008b'>simpl</span> <span style='color:#228b22'>in</span> *.\n\n<hr />\n  m : nat\n  x : t m\n  t : t m\n  H : inr x = inr t\n  ============================\n   t = x\n\nsubgoal 2 (ID 1022) is:\n FS (R n t) = x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
induction n; intros; simpl in *.

\$(function () {
\$("#context-56").tooltip({
content: "<pre><code>  m : nat\n  x : t m\n  t : t m\n  H : inr x = inr t\n  ============================\n   t = x\n\n<hr />\n  <span style='color:#ff0000'>congruence</span>.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- congruence.

\$(function () {
\$("#context-57").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  x : t (S (n + m))\n  t : t m\n  H : fin_case (n + m) x\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inr t\n  ============================\n   FS (R n t) = x\n\n<hr />\n  <span style='color:#00008b'>revert</span> H.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  x : t (S (n + m))\n  t : t m\n  ============================\n   fin_case (n + m) x\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inr t -> FS (R n t) = x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- revert H.

\$(function () {
\$("#context-58").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  x : t (S (n + m))\n  t : t m\n  ============================\n   fin_case (n + m) x\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n     (inl F1)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n      <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span>) = inr t -> FS (R n t) = x\n\n<hr />\n    fin_dep_destruct x.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  H : fin_case (n + m) F1\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inr t\n  ============================\n   FS (R n t) = F1\n\nsubgoal 2 (ID 1033) is:\n FS (R n t) = FS y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
fin_dep_destruct x.

\$(function () {
\$("#context-59").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  H : fin_case (n + m) F1\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inr t\n  ============================\n   FS (R n t) = F1\n\n<hr />\n    <span style='color:#ff0000'>discriminate</span>.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ discriminate.

\$(function () {
\$("#context-60").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  H : fin_case (n + m) (FS y)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) =<span style='color:#a0522d'>></span> (<span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) + <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>)<span style='color:#a0522d'>%type</span>)\n        (inl F1)\n        (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>) =<span style='color:#a0522d'>></span>\n         <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x' <span style='color:#228b22'>with</span>\n         | inl a => inl (FS a)\n         | inr b => inr b\n         <span style='color:#228b22'>end</span>) = inr t\n  ============================\n   FS (R n t) = FS y\n\n<hr />\n    <span style='color:#00008b'>simpl</span> <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin y <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span> = inr t\n  ============================\n   FS (R n t) = FS y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ simpl in *.

\$(function () {
\$("#context-61").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin y <span style='color:#228b22'>with</span>\n      | inl a => inl (FS a)\n      | inr b => inr b\n      <span style='color:#228b22'>end</span> = inr t\n  ============================\n   FS (R n t) = FS y\n\n<hr />\n      break_match.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  t0 : Fin.t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  H : inl (FS t0) = inr t\n  ============================\n   FS (R n t) = FS y\n\nsubgoal 2 (ID 1064) is:\n FS (R n t) = FS y\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
break_match.

\$(function () {
\$("#context-62").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  t0 : Fin.t n\n  Heqs : fin_of_sum_to_sum_of_fin y = inl t0\n  H : inl (FS t0) = inr t\n  ============================\n   FS (R n t) = FS y\n\n<hr />\n      <span style='color:#ff0000'>discriminate</span>.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
* discriminate.

\$(function () {
\$("#context-63").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  t0 : Fin.t m\n  Heqs : fin_of_sum_to_sum_of_fin y = inr t0\n  H : inr t0 = inr t\n  ============================\n   FS (R n t) = FS y\n\n<hr />\n      f_equal.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  t0 : Fin.t m\n  Heqs : fin_of_sum_to_sum_of_fin y = inr t0\n  H : inr t0 = inr t\n  ============================\n   R n t = y\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
* f_equal.

\$(function () {
\$("#context-64").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> + <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>t</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_sum_to_sum_of_fin x = inr t -> R n t = x\n  m : nat\n  t : t m\n  y : Fin.t (n + m)\n  t0 : Fin.t m\n  Heqs : fin_of_sum_to_sum_of_fin y = inr t0\n  H : inr t0 = inr t\n  ============================\n   R n t = y\n\n<hr />\n        solve_by_inversion.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
solve_by_inversion.
Qed.
``````

We can finally complete the proof of the second direction

``````
\$(function () {
\$("#context-65").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : t (n + m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f1 (f2 x0) = x0\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x0</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g1 (g2 x0) = x0\n  t : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  ============================\n   R n t = x\n\n<hr />\n   <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> R_fin_of_sum_to_sum_of_fin.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using R_fin_of_sum_to_sum_of_fin.
Qed.
``````

Now that we know `to_sum` and `from_sum` are inverses, we can prove the desired result about cardinalities of sums.

``````    Lemma card_sum :
forall A B m n,
cardinality A m ->
cardinality B n ->
cardinality (A + B) (m + n).
Proof.

\$(function () {
\$("#context-66").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>m</span> <span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   cardinality A m -> cardinality B n -> cardinality (A + B) (m + n)\n\n\n<hr />\n  <span style='color:#00008b'>unfold</span> cardinality.\n\n<hr />\n  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>m</span> <span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   (<span style='color:#00008b'>exists</span> (to_fin : A -> t m) (from_fin : t m -> A),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, to_fin (from_fin y) = y)) ->\n   (<span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)) ->\n   <span style='color:#00008b'>exists</span> (to_fin : A + B -> t (m + n)) (from_fin : t (m + n) -> A + B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold cardinality.

\$(function () {
\$("#context-67").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>m</span> <span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   (<span style='color:#00008b'>exists</span> (to_fin : A -> t m) (from_fin : t m -> A),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, to_fin (from_fin y) = y)) ->\n   (<span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)) ->\n   <span style='color:#00008b'>exists</span> (to_fin : A + B -> t (m + n)) (from_fin : t (m + n) -> A + B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>firstorder</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : A + B -> t (m + n)) (from_fin : t (m + n) -> A + B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, from_fin (to_fin x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
firstorder.

\$(function () {
\$("#context-68").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : A + B -> t (m + n)) (from_fin : t (m + n) -> A + B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, from_fin (to_fin x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>eexists</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> from_fin : t (m + n) -> A + B,\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, from_fin (?1186 x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), ?1186 (from_fin y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
eexists.

\$(function () {
\$("#context-69").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> from_fin : t (m + n) -> A + B,\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, from_fin (?1186 x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), ?1186 (from_fin y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>eexists</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, ?1189 (?1186 x3) = x3) /\\\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), ?1186 (?1189 y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
eexists.

\$(function () {
\$("#context-70").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> + <span style='color:#a0522d'>B</span>, ?1189 (?1186 x3) = x3) /\\\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span>), ?1186 (?1189 y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>eauto</span> <span style='color:#228b22'>using</span> to_from_sum, from_to_sum.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
eauto using to_from_sum, from_to_sum.
Qed.
``````

We now prove that the cardinality of a product of types is the product of the cardinalities. First, we define the isomorphisms at the `Fin.t` level.

The first direction takes two `Fin.t`s and encodes them in a larger `Fin.t`. This is analogous to the `L` and `R` operations (from the standard library) that we used above to convert sums. Conceptually, we divide `Fin.t (n * m)` into `n` blocks of `m` elements each. The value of `x` tells us which block we’re in, and the value of `y` tells us which element in the block. In the case where `n = S n''` for some `n''`, `(S n'') * m` simplifies to `m + n'' * m`. This lets us use `L` and `R` to inject into the left or right side of the sum.

``````    Fixpoint prod_of_fin_to_fin_of_prod {n m} {struct n} :
Fin.t n ->  Fin.t m -> Fin.t (n * m) :=
match n as n' return Fin.t n' -> Fin.t m -> Fin.t (n' * m) with
| 0 => fun x _ => case0 _ x
| S n'' =>
fun x y =>
fin_case _ x _
(L _ y)
(fun x' => R _ (prod_of_fin_to_fin_of_prod x' y))
end.
``````

In the other direction, when `n = S n'`, we again have a `Fin.t` of a sum, and we use the conversion function for sums to decide whether the argument is in the “current” block (the left part of the sum) or some later block.

``````    Fixpoint fin_of_prod_to_prod_of_fin {n m} {struct n} :
Fin.t (n * m) -> Fin.t n * Fin.t m :=
match n as n' return Fin.t (n' * m) -> Fin.t n' * Fin.t m with
| 0 => fun x => case0 _ x
| S n' =>
fun x =>
match fin_of_sum_to_sum_of_fin x with
| inl a => (F1, a)
| inr b => let (x,y) := fin_of_prod_to_prod_of_fin b
in (FS x, y)
end
end.
``````

Then given encode/decode functions on the underlying types, we can define encode/decode functions on pairs.

``````    Definition from_prod {n m A B} (f : A -> Fin.t n) (g : B -> Fin.t m)
(x : A * B) : Fin.t (n * m) :=
let (a,b) := x in
prod_of_fin_to_fin_of_prod (f a) (g b).

Definition to_prod {n m A B} (f : Fin.t n -> A) (g : Fin.t m -> B)
(x : Fin.t (n * m)) : A * B :=
let (a,b) := fin_of_prod_to_prod_of_fin x in (f a, g b).
``````

We now need lemmas showing these functions are inverses. Because the implementation uses some lemmas about encoding and decoding, we’ll need to use the relevant lemmas in our proofs. We first show that the isomorphism between products of `Fin.t`s and `Fin.t`s of products is actually an isomorphism.

``````    Lemma fin_prod_fin_inverse :
forall n m x a b,
@fin_of_prod_to_prod_of_fin n m x = (a,b) ->
prod_of_fin_to_fin_of_prod a b = x.
Proof.

\$(function () {
\$("#context-71").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n   fin_of_prod_to_prod_of_fin x = (a, b) ->\n   prod_of_fin_to_fin_of_prod a b = x\n\n\n<hr />\n  <span style='color:#00008b'>induction</span> n; <span style='color:#00008b'>intros</span>.\n\n<hr />\n  m : nat\n  x : t (0 * m)\n  a : t 0\n  b : t m\n  H : fin_of_prod_to_prod_of_fin x = (a, b)\n  ============================\n   prod_of_fin_to_fin_of_prod a b = x\n\nsubgoal 2 (ID 1321) is:\n prod_of_fin_to_fin_of_prod a b = x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
induction n; intros.

\$(function () {
\$("#context-72").tooltip({
content: "<pre><code>  m : nat\n  x : t (0 * m)\n  a : t 0\n  b : t m\n  H : fin_of_prod_to_prod_of_fin x = (a, b)\n  ============================\n   prod_of_fin_to_fin_of_prod a b = x\n\nsubgoal 2 (ID 1321) is:\n prod_of_fin_to_fin_of_prod a b = x\n\n<hr />\n  solve_by_inversion.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- solve_by_inversion.

\$(function () {
\$("#context-73").tooltip({
content: "<pre><code>subgoal 1 (ID 1321) is:\n prod_of_fin_to_fin_of_prod a b = x\n\n<hr />\n  <span style='color:#00008b'>simpl</span> <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x <span style='color:#228b22'>with</span>\n      | inl a0 => (F1, a0)\n      | inr b0 => <span style='color:#228b22'>let</span> (x0, y) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x0, y)\n      <span style='color:#228b22'>end</span> = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L\n        ((fix mult (n0 m0 : nat) {struct n0} : nat :=\n            <span style='color:#228b22'>match</span> n0 <span style='color:#228b22'>with</span>\n            | 0 => 0\n            | S p => m0 + mult p m0\n            <span style='color:#228b22'>end</span>) n m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- simpl in *.

\$(function () {
\$("#context-74").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x <span style='color:#228b22'>with</span>\n      | inl a0 => (F1, a0)\n      | inr b0 => <span style='color:#228b22'>let</span> (x0, y) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x0, y)\n      <span style='color:#228b22'>end</span> = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L\n        ((fix mult (n0 m0 : nat) {struct n0} : nat :=\n            <span style='color:#228b22'>match</span> n0 <span style='color:#228b22'>with</span>\n            | 0 => 0\n            | S p => m0 + mult p m0\n            <span style='color:#228b22'>end</span>) n m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n<hr />\n    <span style='color:#00008b'>fold</span> mult <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x <span style='color:#228b22'>with</span>\n      | inl a0 => (F1, a0)\n      | inr b0 => <span style='color:#228b22'>let</span> (x0, y) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x0, y)\n      <span style='color:#228b22'>end</span> = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) =\n   x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
fold mult in *.

\$(function () {
\$("#context-75").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  H : <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin x <span style='color:#228b22'>with</span>\n      | inl a0 => (F1, a0)\n      | inr b0 => <span style='color:#228b22'>let</span> (x0, y) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x0, y)\n      <span style='color:#228b22'>end</span> = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) =\n   x\n\n<hr />\n    break_match.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
break_match.

\$(function () {
\$("#context-76").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  t : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inl t\n  H : (F1, t) = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n<hr />\n    find_inversion.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inl b\n  ============================\n   fin_case n F1 (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) =\n   x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ find_inversion.

\$(function () {
\$("#context-77").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inl b\n  ============================\n   fin_case n F1 (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) =\n   x\n\n<hr />\n      <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inl b\n  ============================\n   L (n * m) b = x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
simpl.

\$(function () {
\$("#context-78").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  Heqs : fin_of_sum_to_sum_of_fin x = inl b\n  ============================\n   L (n * m) b = x\n\n<hr />\n      <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> L_fin_of_sum_to_sum_of_fin.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using L_fin_of_sum_to_sum_of_fin.

\$(function () {
\$("#context-79").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  H : (<span style='color:#228b22'>let</span> (x0, y) := fin_of_prod_to_prod_of_fin t <span style='color:#228b22'>in</span> (FS x0, y)) = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n<hr />\n    break_match.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  t1 : Fin.t m\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, t1)\n  H : (FS t0, t1) = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ break_match.

\$(function () {
\$("#context-80").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  a : t (S n)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  t1 : Fin.t m\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, t1)\n  H : (FS t0, t1) = (a, b)\n  ============================\n   fin_case n a (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n<hr />\n      find_inversion.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, b)\n  ============================\n   fin_case n (FS t0) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_inversion.

\$(function () {
\$("#context-81").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, b)\n  ============================\n   fin_case n (FS t0) (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>_</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>S</span> <span style='color:#a0522d'>n</span>) =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> + <span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>))\n     (L (n * m) b)\n     (<span style='color:#228b22'>fun</span> <span style='color:#a0522d'>x'</span> : <span style='color:#a0522d'>Fin</span>.<span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> =<span style='color:#a0522d'>></span> <span style='color:#a0522d'>R</span> <span style='color:#a0522d'>m</span> (<span style='color:#a0522d'>prod_of_fin_to_fin_of_prod</span> <span style='color:#a0522d'>x'</span> <span style='color:#a0522d'>b</span>)) = <span style='color:#a0522d'>x</span>\n\n<hr />\n      <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, b)\n  ============================\n   R m (prod_of_fin_to_fin_of_prod t0 b) = x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
simpl.

\$(function () {
\$("#context-82").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, b)\n  ============================\n   R m (prod_of_fin_to_fin_of_prod t0 b) = x\n\n<hr />\n      <span style='color:#00008b'>erewrite</span> IHn; <span style='color:#00008b'>eauto</span>.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, b)\n  ============================\n   R m t = x\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
erewrite IHn; eauto.

\$(function () {
\$("#context-83").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>n</span> * <span style='color:#a0522d'>m</span>)) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin x = (a, b) ->\n        prod_of_fin_to_fin_of_prod a b = x\n  m : nat\n  x : t (m + n * m)\n  b : t m\n  t : t (n * m)\n  Heqs : fin_of_sum_to_sum_of_fin x = inr t\n  t0 : Fin.t n\n  Heqp : fin_of_prod_to_prod_of_fin t = (t0, b)\n  ============================\n   R m t = x\n\n<hr />\n      <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> R_fin_of_sum_to_sum_of_fin.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using R_fin_of_sum_to_sum_of_fin.
Qed.

Lemma prod_fin_prod_inverse :
forall n m a b,
@fin_of_prod_to_prod_of_fin n m (prod_of_fin_to_fin_of_prod a b) = (a,b).
Proof.

\$(function () {
\$("#context-84").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n   fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n\n\n<hr />\n  <span style='color:#00008b'>induction</span> n; <span style='color:#00008b'>intros</span>.\n\n<hr />\n  m : nat\n  a : t 0\n  b : t m\n  ============================\n   fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n\nsubgoal 2 (ID 1564) is:\n fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
induction n; intros.

\$(function () {
\$("#context-85").tooltip({
content: "<pre><code>  m : nat\n  a : t 0\n  b : t m\n  ============================\n   fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n\n<hr />\n  solve_by_inversion.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- solve_by_inversion.

\$(function () {
\$("#context-86").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  a : t (S n)\n  b : t m\n  ============================\n   fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n\n<hr />\n  fin_dep_destruct a; <span style='color:#00008b'>simpl</span>.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  ============================\n   <span style='color:#228b22'>match</span>\n     fin_of_sum_to_sum_of_fin\n       (L\n          ((fix mult (n0 m0 : nat) {struct n0} : nat :=\n              <span style='color:#228b22'>match</span> n0 <span style='color:#228b22'>with</span>\n              | 0 => 0\n              | S p => m0 + mult p m0\n              <span style='color:#228b22'>end</span>) n m) b)\n   <span style='color:#228b22'>with</span>\n   | inl a => (F1, a)\n   | inr b0 => <span style='color:#228b22'>let</span> (x, y) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x, y)\n   <span style='color:#228b22'>end</span> = (F1, b)\n\nsubgoal 2 (ID 1634) is:\n <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (R m (prod_of_fin_to_fin_of_prod y b)) <span style='color:#228b22'>with</span>\n | inl a => (F1, a)\n | inr b0 => <span style='color:#228b22'>let</span> (x, y0) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x, y0)\n <span style='color:#228b22'>end</span> = (FS y, b)\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
- fin_dep_destruct a; simpl.

\$(function () {
\$("#context-87").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  ============================\n   <span style='color:#228b22'>match</span>\n     fin_of_sum_to_sum_of_fin\n       (L\n          ((fix mult (n0 m0 : nat) {struct n0} : nat :=\n              <span style='color:#228b22'>match</span> n0 <span style='color:#228b22'>with</span>\n              | 0 => 0\n              | S p => m0 + mult p m0\n              <span style='color:#228b22'>end</span>) n m) b)\n   <span style='color:#228b22'>with</span>\n   | inl a => (F1, a)\n   | inr b0 => <span style='color:#228b22'>let</span> (x, y) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x, y)\n   <span style='color:#228b22'>end</span> = (F1, b)\n\n<hr />\n    <span style='color:#00008b'>rewrite</span> fin_of_sum_to_sum_of_fin_L <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  ============================\n   (F1, b) = (F1, b)\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ rewrite fin_of_sum_to_sum_of_fin_L in *.

\$(function () {
\$("#context-88").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  ============================\n   (F1, b) = (F1, b)\n\n<hr />\n      <span style='color:#00008b'>auto</span>.\n\n<hr />\nThis subproof is complete, but there are still unfocused goals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto.

\$(function () {
\$("#context-89").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  y : t n\n  ============================\n   <span style='color:#228b22'>match</span> fin_of_sum_to_sum_of_fin (R m (prod_of_fin_to_fin_of_prod y b)) <span style='color:#228b22'>with</span>\n   | inl a => (F1, a)\n   | inr b0 => <span style='color:#228b22'>let</span> (x, y0) := fin_of_prod_to_prod_of_fin b0 <span style='color:#228b22'>in</span> (FS x, y0)\n   <span style='color:#228b22'>end</span> = (FS y, b)\n\n<hr />\n    <span style='color:#00008b'>rewrite</span> fin_of_sum_to_sum_of_fin_R <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  y : t n\n  ============================\n   (<span style='color:#228b22'>let</span> (x, y0) :=\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod y b) <span style='color:#228b22'>in</span>\n    (FS x, y0)) = (FS y, b)\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
+ rewrite fin_of_sum_to_sum_of_fin_R in *.

\$(function () {
\$("#context-90").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  y : t n\n  ============================\n   (<span style='color:#228b22'>let</span> (x, y0) :=\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod y b) <span style='color:#228b22'>in</span>\n    (FS x, y0)) = (FS y, b)\n\n<hr />\n      <span style='color:#00008b'>rewrite</span> IHn.\n\n<hr />\n  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  y : t n\n  ============================\n   (FS y, b) = (FS y, b)\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
rewrite IHn.

\$(function () {
\$("#context-91").tooltip({
content: "<pre><code>  n : nat\n  IHn : <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>a</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>) (<span style='color:#a0522d'>b</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>),\n        fin_of_prod_to_prod_of_fin (prod_of_fin_to_fin_of_prod a b) = (a, b)\n  m : nat\n  b : t m\n  y : t n\n  ============================\n   (FS y, b) = (FS y, b)\n\n<hr />\n      <span style='color:#00008b'>auto</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto.
Qed.
``````

We now show that the encode/decode functions are inverses.

``````    Lemma from_to_prod :
forall n m A B f1 f2 g1 g2 x,
(forall y, f2 (f1 y) = y) ->
(forall y, g2 (g1 y) = y) ->
from_prod f2 g2 (@to_prod n m A B f1 g1 x) = x.
Proof.

\$(function () {
\$("#context-92").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f1</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>A</span>)\n     (f2 : A -> t n) (g1 : t m -> B) (g2 : B -> t m)\n     (x : t (n * m)),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y) -> from_prod f2 g2 (to_prod f1 g1 x) = x\n\n\n<hr />\n  <span style='color:#00008b'>intros</span>.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  ============================\n   from_prod f2 g2 (to_prod f1 g1 x) = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
intros.

\$(function () {
\$("#context-93").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  ============================\n   from_prod f2 g2 (to_prod f1 g1 x) = x\n\n\n<hr />\n  <span style='color:#00008b'>unfold</span> from_prod, to_prod.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  ============================\n   (<span style='color:#228b22'>let</span> (a, b) :=\n        <span style='color:#228b22'>let</span> (a, b) := fin_of_prod_to_prod_of_fin x <span style='color:#228b22'>in</span> (f1 a, g1 b) <span style='color:#228b22'>in</span>\n    prod_of_fin_to_fin_of_prod (f2 a) (g2 b)) = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold from_prod, to_prod.

\$(function () {
\$("#context-94").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  ============================\n   (<span style='color:#228b22'>let</span> (a, b) :=\n        <span style='color:#228b22'>let</span> (a, b) := fin_of_prod_to_prod_of_fin x <span style='color:#228b22'>in</span> (f1 a, g1 b) <span style='color:#228b22'>in</span>\n    prod_of_fin_to_fin_of_prod (f2 a) (g2 b)) = x\n\n\n<hr />\n  <span style='color:#a020f0'>repeat</span> break_match.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  Heqp : (f1 t, g1 t0) = (a, b)\n  ============================\n   prod_of_fin_to_fin_of_prod (f2 a) (g2 b) = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
repeat break_match.

\$(function () {
\$("#context-95").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  Heqp : (f1 t, g1 t0) = (a, b)\n  ============================\n   prod_of_fin_to_fin_of_prod (f2 a) (g2 b) = x\n\n\n<hr />\n  find_inversion.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  ============================\n   prod_of_fin_to_fin_of_prod (f2 (f1 t)) (g2 (g1 t0)) = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_inversion.

\$(function () {
\$("#context-96").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  ============================\n   prod_of_fin_to_fin_of_prod (f2 (f1 t)) (g2 (g1 t0)) = x\n\n\n<hr />\n  find_higher_order_rewrite.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  ============================\n   prod_of_fin_to_fin_of_prod (f2 (f1 t)) t0 = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_higher_order_rewrite.

\$(function () {
\$("#context-97").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  ============================\n   prod_of_fin_to_fin_of_prod (f2 (f1 t)) t0 = x\n\n\n<hr />\n  find_higher_order_rewrite.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  ============================\n   prod_of_fin_to_fin_of_prod t t0 = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_higher_order_rewrite.

\$(function () {
\$("#context-98").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : t n -> A\n  f2 : A -> t n\n  g1 : t m -> B\n  g2 : B -> t m\n  x : t (n * m)\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  Heqp0 : fin_of_prod_to_prod_of_fin x = (t, t0)\n  ============================\n   prod_of_fin_to_fin_of_prod t t0 = x\n\n\n<hr />\n  <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> fin_prod_fin_inverse.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using fin_prod_fin_inverse.
Qed.

Lemma to_from_prod :
forall n m A B f1 f2 g1 g2 x,
(forall y, f2 (f1 y) = y) ->
(forall y, g2 (g1 y) = y) ->
to_prod f2 g2 (@from_prod n m A B f1 g1 x) = x.
Proof.

\$(function () {
\$("#context-99").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>n</span> <span style='color:#a0522d'>m</span> : <span style='color:#a0522d'>nat</span>) (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>f1</span> : <span style='color:#a0522d'>A</span> -<span style='color:#a0522d'>></span> <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>)\n     (f2 : t n -> A) (g1 : B -> t m) (g2 : t m -> B)\n     (x : A * B),\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y) ->\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y) -> to_prod f2 g2 (from_prod f1 g1 x) = x\n\n\n<hr />\n  <span style='color:#00008b'>intros</span>.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A * B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  ============================\n   to_prod f2 g2 (from_prod f1 g1 x) = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
intros.

\$(function () {
\$("#context-100").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A * B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  ============================\n   to_prod f2 g2 (from_prod f1 g1 x) = x\n\n\n<hr />\n  <span style='color:#00008b'>unfold</span> from_prod, to_prod.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A * B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  ============================\n   (<span style='color:#228b22'>let</span> (a, b) :=\n        fin_of_prod_to_prod_of_fin\n          (<span style='color:#228b22'>let</span> (a, b) := x <span style='color:#228b22'>in</span> prod_of_fin_to_fin_of_prod (f1 a) (g1 b)) <span style='color:#228b22'>in</span>\n    (f2 a, g2 b)) = x\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold from_prod, to_prod.

\$(function () {
\$("#context-101").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A * B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  ============================\n   (<span style='color:#228b22'>let</span> (a, b) :=\n        fin_of_prod_to_prod_of_fin\n          (<span style='color:#228b22'>let</span> (a, b) := x <span style='color:#228b22'>in</span> prod_of_fin_to_fin_of_prod (f1 a) (g1 b)) <span style='color:#228b22'>in</span>\n    (f2 a, g2 b)) = x\n\n\n<hr />\n  <span style='color:#a020f0'>repeat</span> break_match.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A * B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  a : A\n  b : B\n  Heqp0 : x = (a, b)\n  Heqp : fin_of_prod_to_prod_of_fin\n           (prod_of_fin_to_fin_of_prod (f1 a) (g1 b)) =\n         (t, t0)\n  ============================\n   (f2 t, g2 t0) = (a, b)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
repeat break_match.

\$(function () {
\$("#context-102").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  x : A * B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  a : A\n  b : B\n  Heqp0 : x = (a, b)\n  Heqp : fin_of_prod_to_prod_of_fin\n           (prod_of_fin_to_fin_of_prod (f1 a) (g1 b)) =\n         (t, t0)\n  ============================\n   (f2 t, g2 t0) = (a, b)\n\n\n<hr />\n  <span style='color:#00008b'>subst</span>.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  a : A\n  b : B\n  Heqp : fin_of_prod_to_prod_of_fin\n           (prod_of_fin_to_fin_of_prod (f1 a) (g1 b)) =\n         (t, t0)\n  ============================\n   (f2 t, g2 t0) = (a, b)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
subst.

\$(function () {
\$("#context-103").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  a : A\n  b : B\n  Heqp : fin_of_prod_to_prod_of_fin\n           (prod_of_fin_to_fin_of_prod (f1 a) (g1 b)) =\n         (t, t0)\n  ============================\n   (f2 t, g2 t0) = (a, b)\n\n\n<hr />\n  <span style='color:#00008b'>rewrite</span> prod_fin_prod_inverse <span style='color:#228b22'>in</span> *.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  a : A\n  b : B\n  Heqp : (f1 a, g1 b) = (t, t0)\n  ============================\n   (f2 t, g2 t0) = (a, b)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
rewrite prod_fin_prod_inverse in *.

\$(function () {
\$("#context-104").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  t : t n\n  t0 : Fin.t m\n  a : A\n  b : B\n  Heqp : (f1 a, g1 b) = (t, t0)\n  ============================\n   (f2 t, g2 t0) = (a, b)\n\n\n<hr />\n  find_inversion.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  ============================\n   (f2 (f1 a), g2 (g1 b)) = (a, b)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_inversion.

\$(function () {
\$("#context-105").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  ============================\n   (f2 (f1 a), g2 (g1 b)) = (a, b)\n\n\n<hr />\n  find_higher_order_rewrite.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  ============================\n   (f2 (f1 a), b) = (a, b)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_higher_order_rewrite.

\$(function () {
\$("#context-106").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  ============================\n   (f2 (f1 a), b) = (a, b)\n\n\n<hr />\n  find_higher_order_rewrite.\n\n<hr />\n  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  ============================\n   (a, b) = (a, b)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
find_higher_order_rewrite.

\$(function () {
\$("#context-107").tooltip({
content: "<pre><code>  n : nat\n  m : nat\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  f1 : A -> t n\n  f2 : t n -> A\n  g1 : B -> t m\n  g2 : t m -> B\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>A</span>, f2 (f1 y) = y\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>B</span>, g2 (g1 y) = y\n  a : A\n  b : B\n  ============================\n   (a, b) = (a, b)\n\n\n<hr />\n  <span style='color:#00008b'>auto</span>.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto.
Qed.
``````

Finally we can show that the cardinality of a product is the product of the cardinalities.

``````    Lemma card_prod :
forall A B m n,
cardinality A m ->
cardinality B n ->
cardinality (A * B) (m * n).
Proof.

\$(function () {
\$("#context-108").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>m</span> <span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   cardinality A m -> cardinality B n -> cardinality (A * B) (m * n)\n\n\n<hr />\n  <span style='color:#00008b'>unfold</span> cardinality.\n\n<hr />\n  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>m</span> <span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   (<span style='color:#00008b'>exists</span> (to_fin : A -> t m) (from_fin : t m -> A),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, to_fin (from_fin y) = y)) ->\n   (<span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)) ->\n   <span style='color:#00008b'>exists</span> (to_fin : A * B -> t (m * n)) (from_fin : t (m * n) -> A * B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
unfold cardinality.

\$(function () {
\$("#context-109").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> <span style='color:#a0522d'>B</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>m</span> <span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   (<span style='color:#00008b'>exists</span> (to_fin : A -> t m) (from_fin : t m -> A),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, to_fin (from_fin y) = y)) ->\n   (<span style='color:#00008b'>exists</span> (to_fin : B -> t n) (from_fin : t n -> B),\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n      (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, to_fin (from_fin y) = y)) ->\n   <span style='color:#00008b'>exists</span> (to_fin : A * B -> t (m * n)) (from_fin : t (m * n) -> A * B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, from_fin (to_fin x) = x) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>firstorder</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : A * B -> t (m * n)) (from_fin : t (m * n) -> A * B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, from_fin (to_fin x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
firstorder.

\$(function () {
\$("#context-110").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> (to_fin : A * B -> t (m * n)) (from_fin : t (m * n) -> A * B),\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, from_fin (to_fin x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), to_fin (from_fin y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>eexists</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> from_fin : t (m * n) -> A * B,\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, from_fin (?1947 x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), ?1947 (from_fin y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
eexists.

\$(function () {
\$("#context-111").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   <span style='color:#00008b'>exists</span> from_fin : t (m * n) -> A * B,\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, from_fin (?1947 x3) = x3) /\\\n     (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), ?1947 (from_fin y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>eexists</span>.\n\n<hr />\n  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, ?1950 (?1947 x3) = x3) /\\\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), ?1947 (?1950 y) = y)\n\n\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
eexists.

\$(function () {
\$("#context-112").tooltip({
content: "<pre><code>  A : <span style='color:#228b22'>Type</span>\n  B : <span style='color:#228b22'>Type</span>\n  m : nat\n  n : nat\n  x : A -> t m\n  x0 : B -> t n\n  x1 : t m -> A\n  H : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x2</span> : <span style='color:#a0522d'>A</span>, x1 (x x2) = x2\n  H1 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>m</span>, x (x1 y) = y\n  x2 : t n -> B\n  H0 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>B</span>, x2 (x0 x3) = x3\n  H2 : <span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> <span style='color:#a0522d'>n</span>, x0 (x2 y) = y\n  ============================\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>x3</span> : <span style='color:#a0522d'>A</span> * <span style='color:#a0522d'>B</span>, ?1950 (?1947 x3) = x3) /\\\n   (<span style='color:#228b22'>forall</span> <span style='color:#a0522d'>y</span> : <span style='color:#a0522d'>t</span> (<span style='color:#a0522d'>m</span> * <span style='color:#a0522d'>n</span>), ?1947 (?1950 y) = y)\n\n\n<hr />\n  <span style='color:#00008b'>eauto</span> <span style='color:#228b22'>using</span> to_from_prod, from_to_prod.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
eauto using to_from_prod, from_to_prod.
Qed.
``````

We now have lemmas explaining how to express `T` as a sum of products, and about the cardinalities of `unit`, and sums and products of `Fin.t`s.

``````    Theorem cardinality_T :
forall A n,
cardinality A n ->
cardinality (T A) (1 + n + n * n).
Proof.

\$(function () {
\$("#context-113").tooltip({
content: "<pre><code>  ============================\n   <span style='color:#228b22'>forall</span> (<span style='color:#a0522d'>A</span> : <span style='color:#a0522d'>Type</span>) (<span style='color:#a0522d'>n</span> : <span style='color:#a0522d'>nat</span>),\n   cardinality A n -> cardinality (T A) (1 + n + n * n)\n\n\n<hr />\n  <span style='color:#00008b'>auto</span> <span style='color:#228b22'>using</span> card_T_sum_prod, card_unit, card_sum, card_prod.\n\n<hr />\nNo more subgoals.\n</code></pre>",
open: function (event, ui) {
ui.tooltip.css('max-width', 'none');
ui.tooltip.css('min-width', '800px');
}
});
});
auto using card_T_sum_prod, card_unit, card_sum, card_prod.
Qed.
``````

Thanks again to `osa1` from the Coq IRC channel for posing this problem. You can see his write up of the problem on his blog.