Show the Proof

import proveit
# Automation is not needed when only showing a stored proof:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%show_proof

	step type	requirements	statement
0	modus ponens	1, 2	⊢
1	instantiation	3	⊢
	:
2	instantiation	33, 4, 5	⊢
	: , :
3	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.fold_forall_natural_pos
4	generalization	6	⊢
5	generalization	7	⊢
6	instantiation	22, 8, 9	⊢
	: , :
7	instantiation	15, 10, 11	, ,  ⊢
	: , : , :
8	instantiation	33, 12, 13	⊢
	: , :
9	instantiation	14	⊢
	: , : , : , :
10	instantiation	15, 16, 17	, ,  ⊢
	: , : , :
11	instantiation	25, 18	⊢
	: , : , :
12	axiom		⊢
	proveit.logic.booleans.true_axiom
13	assumption		⊢
14	instantiation	36, 53, 19*, 20*, 21*	⊢
	:
15	theorem		⊢
	proveit.logic.equality.sub_right_side_into
16	instantiation	22, 23, 24	, ,  ⊢
	: , :
17	instantiation	25, 26	⊢
	: , : , :
18	instantiation	74, 75	⊢
	: , :
19	instantiation	28, 53, 82, 54, 27, 41	⊢
	: , : , : , : , : , : , :
20	instantiation	28, 53, 82, 54, 29, 42	⊢
	: , : , : , : , : , : , :
21	instantiation	30, 31, 32	⊢
	: , : , :
22	theorem		⊢
	proveit.logic.equality.lhs_via_equality
23	instantiation	33, 34, 35	, ,  ⊢
	: , :
24	instantiation	36, 75	⊢
	: , : , : , : , :
25	theorem		⊢
	proveit.core_expr_types.tuples.merge_extension
26	instantiation	74, 75	⊢
	: , :
27	instantiation	66, 53	⊢
	: , :
28	theorem		⊢
	proveit.core_expr_types.tuples.tuple_portion_substitution
29	instantiation	66, 53	⊢
	: , :
30	axiom		⊢
	proveit.logic.equality.equals_transitivity
31	instantiation	37, 38, 39, 40, 41, 42	⊢
	: , : , : , :
32	instantiation	43, 44	⊢
	:
33	theorem		⊢
	proveit.logic.booleans.conjunction.and_if_both
34	instantiation	45, 46	, ,  ⊢
	: , :
35	instantiation	47, 75, 53, 55, 54, 56	,  ⊢
	: , : , : , : , :
36	axiom		⊢
	proveit.core_expr_types.tuples.tuple_eq_def
37	axiom		⊢
	proveit.core_expr_types.operations.operands_substitution
38	theorem		⊢
	proveit.numbers.numerals.decimals.nat2
39	instantiation	48	⊢
	: , :
40	instantiation	48	⊢
	: , :
41	instantiation	49, 50	⊢
	: , : , :
42	instantiation	49, 50	⊢
	: , : , :
43	axiom		⊢
	proveit.logic.booleans.eq_true_intro
44	instantiation	51	⊢
	:
45	assumption		⊢
46	instantiation	52, 53, 75, 82, 54, 55, 56	,  ⊢
	: , : , : , : , : , :
47	theorem		⊢
	proveit.logic.booleans.conjunction.any_from_and
48	theorem		⊢
	proveit.numbers.numerals.decimals.tuple_len_2_typical_eq
49	axiom		⊢
	proveit.core_expr_types.tuples.empty_range_def
50	instantiation	57, 58	⊢
	:
51	axiom		⊢
	proveit.logic.equality.equals_reflexivity
52	theorem		⊢
	proveit.logic.booleans.conjunction.some_from_and
53	axiom		⊢
	proveit.numbers.number_sets.natural_numbers.zero_in_nats
54	theorem		⊢
	proveit.core_expr_types.tuples.tuple_len_0_typical_eq
55	instantiation	66, 75	⊢
	: , :
56	instantiation	59, 67, 60, 61, 62, 63	,  ⊢
	: , : , : , :
57	theorem		⊢
	proveit.numbers.addition.elim_zero_left
58	instantiation	80, 64, 65	⊢
	: , : , :
59	theorem		⊢
	proveit.logic.equality.sub_in_right_operands_via_tuple
60	instantiation	66, 67	⊢
	: , :
61	instantiation	68, 75	⊢
	: , : , :
62	assumption		⊢
63	instantiation	69, 70	⊢
	: , : , :
64	theorem		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
65	instantiation	80, 71, 72	⊢
	: , : , :
66	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_typical_eq
67	instantiation	73, 75, 82	⊢
	: , :
68	theorem		⊢
	proveit.core_expr_types.tuples.extended_range_from1_len_typical_eq
69	axiom		⊢
	proveit.core_expr_types.tuples.range_extension_def
70	instantiation	74, 75	⊢
	: , :
71	theorem		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
72	instantiation	80, 76, 77	⊢
	: , : , :
73	theorem		⊢
	proveit.numbers.addition.add_nat_closure_bin
74	theorem		⊢
	proveit.core_expr_types.tuples.range_from1_len_is_nat
75	instantiation	80, 78, 79	⊢
	: , : , :
76	theorem		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
77	instantiation	80, 81, 82	⊢
	: , : , :
78	theorem		⊢
	proveit.numbers.number_sets.natural_numbers.nat_pos_within_nat
79	assumption		⊢
80	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
81	theorem		⊢
	proveit.numbers.number_sets.integers.nat_within_int
82	theorem		⊢
	proveit.numbers.numerals.decimals.nat1
*equality replacement requirements