proposition: Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl.
proof: Proof. intros a'; induction a' as [|a a' IHa']; simpl. - intros a cl H. destruct (deduce (fst a) (fst a)) as [t|]. + destruct (unsat t). * congruence. * inversion H. reflexivity. + inversion H ;reflexivity. - intros a0 cl H. destruct (deduce (fst a0) (fst a)) as [t|]. + destruct (unsat t). * congruence. * destruct (add_term a0 a') eqn:RADD; try congruence. inversion H. subst. apply IHa' in RADD. rewrite RADD. reflexivity. + destruct (add_term a0 a') eqn:RADD; try congruence. inversion H. subst. apply IHa' in RADD. rewrite RADD. reflexivity. Qed.
imports: List Refl Bool Relation_Definitions Setoid