Let k be given.
rewrite the current goal using
SNo_recipaux_S x g k Hk (from left to right).
rewrite the current goal using
SNo_recipaux_S x h k Hk (from left to right).
rewrite the current goal using IH (from left to right).
Use f_equal.
Use f_equal.
Let w be given.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2.
Let w be given.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2.
Use f_equal.
Use f_equal.
Let w be given.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2.
Let w be given.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply Hgh to the current goal.
An
exact proof term for the current goal is
SNoS_I2 w x Hw1 Hx Hw2.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using L2 (from left to right).
Use reflexivity.
∎