status	milestone	kind	name	file
proved	M1	infra	at_ctx_comp	theory/Reduction.v
proved	M1	infra	close_rec_fvar	theory/Binding.v
proved	M1	infra	close_rec_fvs	theory/Binding.v
proved	M1	infra	close_rec_notin	theory/Binding.v
proved	M1	infra	fvs_lift	theory/Binding.v
proved	M1	infra	has_red_f	theory/Reduction.v
proved	M1	infra	has_red_spec	theory/Reduction.v
proved	M1	infra	lift_0_lc	theory/Binding.v
proved	M1	infra	lift_lc	theory/Binding.v
proved	M1	infra	nf_dec	theory/Reduction.v
proved	M1	infra	nf_iff_steps_nil	theory/Reduction.v
proved	M1	infra	normal_form_iff_nf	theory/Reduction.v
proved	M1	infra	open_close	theory/Binding.v
proved	M1	infra	open_rec_bvar	theory/Binding.v
proved	M1	infra	open_rec_bvar_neq	theory/Binding.v
proved	M1	infra	open_rec_fvs	theory/Binding.v
proved	M1	infra	open_rec_occurs_false	theory/Binding.v
proved	M1	infra	plug_comp	theory/Reduction.v
proved	M1	infra	positions_at	theory/Reduction.v
proved	M1	infra	positions_comp	theory/Reduction.v
proved	M1	infra	positions_hole	theory/Reduction.v
proved	M1	infra	red1_dec	theory/Reduction.v
proved	M1	infra	root_steps_complete	theory/Reduction.v
proved	M1	infra	root_steps_in_steps	theory/Reduction.v
proved	M1	infra	root_steps_sound	theory/Reduction.v
proved	M1	infra	steps_complete	theory/Reduction.v
proved	M1	infra	steps_sound	theory/Reduction.v
proved	M1	infra	steps_sound_red1	theory/Reduction.v
proved	M1	infra	subst_fvar_other	theory/Binding.v
proved	M1	infra	subst_fvar_self	theory/Binding.v
proved	M1	infra	subst_fvs	theory/Binding.v
proved	M1	infra	zdecs_complete	theory/Reduction.v
proved	M1	infra	zdecs_sound	theory/Reduction.v
proved	M2	infra	Plus_red1_context	theory/Metatheory.v
proved	M2	infra	Plus_step_trans	theory/Metatheory.v
proved	M2	infra	Plus_to_Star	theory/Closure.v
proved	M2	infra	Plus_trans	theory/Metatheory.v
proved	M2	infra	Star_red1_context	theory/Closure.v
proved	M2	infra	Star_trans	theory/Closure.v
proved	M2	infra	check_all_true	theory/Random.v
proved	M2	infra	check_term_true	theory/Random.v
proved	M2	infra	close_rec_app	theory/Substitution.v
proved	M2	infra	close_rec_esub	theory/Substitution.v
proved	M2	infra	close_rec_lam	theory/Substitution.v
proved	M2	infra	corpus_complete	theory/Tests.v
proved	M2	infra	corpus_decides	theory/Tests.v
proved	M2	infra	corpus_fv_preserved	theory/Tests.v
proved	M2	infra	corpus_sound	theory/Tests.v
proved	M2	infra	enumerate_check	theory/Enumerate.v
proved	M2	infra	enumerate_complete	theory/Enumerate.v
proved	M2	infra	enumerate_sound	theory/Enumerate.v
proved	M2	infra	full_comp_aux	theory/Metatheory.v
proved	M2	infra	fvs_zplug_lift	theory/Metatheory.v
proved	M2	infra	gen_complete	theory/Random.v
proved	M2	infra	gen_fv_preserved	theory/Random.v
proved	M2	infra	gen_list_length	theory/Random.v
proved	M2	infra	gen_sound	theory/Random.v
proved	M2	infra	in_comb	theory/Enumerate.v
proved	M2	paper	lemma_2_1_fv_preserved	theory/Metatheory.v
proved	M2	paper	lemma_2_2_full_comp	theory/Metatheory.v
proved	M2	paper	lemma_2_3_beta_sim	theory/Metatheory.v
proved	M2	infra	occurs_count_false	theory/Metatheory.v
proved	M2	infra	occurs_count_pos	theory/Metatheory.v
proved	M2	infra	occurs_count_zero	theory/Metatheory.v
proved	M2	infra	occurs_count_zfill_plug	theory/Metatheory.v
proved	M2	infra	occurs_lift_self	theory/Metatheory.v
proved	M2	infra	open_rec_app	theory/Substitution.v
proved	M2	infra	open_rec_esub	theory/Substitution.v
proved	M2	infra	open_rec_lam	theory/Substitution.v
proved	M2	infra	open_rec_lc	theory/Substitution.v
proved	M2	infra	open_rec_lc_atom	theory/Substitution.v
proved	M2	infra	open_rec_zplug_lift	theory/Metatheory.v
proved	M2	infra	plug_fv_mono	theory/Metatheory.v
proved	M2	infra	pow2_pos	theory/Enumerate.v
proved	M2	infra	red1_root_fv	theory/Metatheory.v
proved	M2	infra	red1_star	theory/Closure.v
proved	M2	infra	red1r_fv	theory/Metatheory.v
proved	M2	infra	size_all_terms	theory/Enumerate.v
proved	M2	infra	star_one_trans	theory/Closure.v
proved	M2	infra	subst_app	theory/Substitution.v
proved	M2	infra	subst_esub	theory/Substitution.v
proved	M2	infra	subst_lam	theory/Substitution.v
proved	M2	infra	subst_lc_self	theory/Substitution.v
proved	M2	infra	subst_notin	theory/Substitution.v
proved	M2	infra	subst_other	theory/Substitution.v
proved	M2	infra	zdecs_nonempty	theory/Metatheory.v
proved	M3	infra	R_Gc_disjoint	theory/Subsystem.v
proved	M3	infra	Star_red_sub_context	theory/Subsystem.v
proved	M3	infra	es_count_plug_mono	theory/Subsystem.v
proved	M3	infra	full_comp_aux_sub	theory/Subsystem.v
proved	M3	infra	occurs_zfill	theory/Subsystem.v
proved	M3	infra	plus_red_sub_full_comp	theory/Subsystem.v
proved	M3	infra	red_gc_measure	theory/Subsystem.v
proved	M3	infra	red_gc_terminates	theory/Subsystem.v
proved	M3	infra	red_gc_to_red_sub	theory/Subsystem.v
proved	M3	infra	red_sub_context	theory/Subsystem.v
proved	M3	infra	red_sub_gc	theory/Subsystem.v
proved	M3	infra	red_sub_r	theory/Subsystem.v
proved	M3	infra	red_sub_root_to_red1	theory/Subsystem.v
proved	M3	infra	red_sub_to_red1	theory/Subsystem.v
proved	M3	infra	star_red_sub_full_comp	theory/Subsystem.v
proved	M3	infra	zfill_occurs0	theory/Subsystem.v
proved	M4	infra	par_context	theory/Parallel.v
proved	M4	infra	par_red1_iff	theory/Parallel.v
proved	M4	infra	par_reflexive	theory/Parallel.v
proved	M4	infra	par_to_red1_or_eq	theory/Parallel.v
proved	M4	infra	red1_in_par	theory/Parallel.v
proved	M4	infra	red1_or_eq_to_par	theory/Parallel.v
