proposition: Lemma synth_deterministic : forall (si : state) (a : ast) (c d : command), synthesis_trans si a c -> synthesis_trans si a d -> c = d.
proof: Proof. simple induction 1; intros. inversion_clear H1. elim equiv_unique with (glob_names si) t e t0; auto with coc core arith datatypes. inversion_clear H2. elim equiv_unique with (glob_names si) m e1 m0; auto with coc core arith datatypes. elim equiv_unique with (glob_names si) t e2 t0; auto with coc core arith datatypes. inversion_clear H1. elim equiv_unique with (glob_names si) t e t0; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. inversion_clear H0; auto with coc core arith datatypes. Qed.
imports: Termes Conv Types Conv_Dec Infer Expr