Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_baf753c31c9c76923012452985368b5d662b0be72d665d17acbd776d20f98e9a with
x0,
or (x0 = 1) (x0 = 2) leaving 4 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_bdf0eb0ad914e7080c1a90c10a5be5aadacffe01a001ae1e9b4568b2273272d9 with
x0,
x1,
x0 ⊆ 2 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Assume H3: x1 = 0.
Apply FalseE with
x0 ⊆ 2.
Apply neq_2_0.
Apply H2 with
λ x2 x3 . x2 = 0.
Apply H3 with
λ x2 x3 . mul_nat x0 x3 = 0.
The subproof is completed by applying mul_nat_0R with x0.
The subproof is completed by applying H2 with λ x2 x3 . x0 ⊆ x2.
Assume H3:
or (x0 = 0) (x0 = 1).
Apply H3 with
or (x0 = 1) (x0 = 2) leaving 2 subgoals.
Assume H4: x0 = 0.
Apply FalseE with
or (x0 = 1) (x0 = 2).
Apply neq_2_0.
Apply H2 with
λ x2 x3 . x2 = 0.
Apply H4 with
λ x2 x3 . mul_nat x3 x1 = 0.
Apply mul_nat_0L with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying orIL with x0 = 1, x0 = 2.
The subproof is completed by applying orIR with x0 = 1, x0 = 2.