I have types B
and A n
where n:nat
. I want to prove that B
is the sum of all A n
. I have three functions
foo (n:nat) (a: A n) : B
rang (b:B) : nat
bar (b:B) : A (rang b)
I can prove
forall (b:B), foo (rang b) (bar b) = b
forall (n:nat) (a: A n), rang (foo n a) = n
But when I write the theorem
forall (n:nat) (a: A n), bar (foo n a) = a
I get "The term bar (foo n a)
has type A (rang (foo n a))
while it is expected to have type A n
".
What can I do?
A,
B,
foo,
rang` etc. are concrete types or variables. As written, without knowing more about them, you cannot prove the desired equalities. There is information that you are not communicating. $\endgroup$