| pf |
|---|
Apply nat_ind with λ x0 . x0 ∈ mul_nat 2 (ordsucc x0) leaving 2 subgoals.
Apply mul_nat_1R with 2, λ x0 x1 . 0 ∈ x1.
The subproof is completed by applying In_0_2.
Let x0 of type ι be given.
Apply mul_nat_SR with 2, ordsucc x0, λ x1 x2 . ordsucc x0 ∈ x2 leaving 2 subgoals.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
Apply mul_nat_p with 2, ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
Apply add_nat_SL with 1, mul_nat 2 (ordsucc x0), λ x1 x2 . ordsucc x0 ∈ x2 leaving 3 subgoals.
The subproof is completed by applying nat_1.
The subproof is completed by applying L2.
Apply add_nat_SL with 0, mul_nat 2 (ordsucc x0), λ x1 x2 . ordsucc x0 ∈ ordsucc x2 leaving 3 subgoals.
The subproof is completed by applying nat_0.
The subproof is completed by applying L2.
Apply add_nat_0L with mul_nat 2 (ordsucc x0), λ x1 x2 . ordsucc x0 ∈ ordsucc (ordsucc x2) leaving 2 subgoals.
The subproof is completed by applying L2.
Apply nat_ordsucc_in_ordsucc with ordsucc (mul_nat 2 (ordsucc x0)), x0 leaving 2 subgoals.
Apply nat_ordsucc with mul_nat 2 (ordsucc x0).
The subproof is completed by applying L2.
Apply ordsuccI1 with mul_nat 2 (ordsucc x0), x0.
The subproof is completed by applying H1.
■ |
|