Inductive truth : Set := Yes | No | Maybe. Definition and t1 t2 := match t1 with | No => No | Maybe => match t2 with No => No | _ => Maybe end | Yes => t1 end. Definition or t1 t2 := match t1 with | No => t2 | Maybe => match t2 with Yes => Yes | _ => Maybe end | Yes => Yes end. Lemma distr : forall t1 t2 t3, and t1 (or t2 t3) = or (and t1 t2) (and t1 t3). (* destruct t1. + simpl. auto. + simpl. auto. + simpl. destruct t2; destruct t3; simpl; trivial. *) destruct t1; destruct t2; destruct t3; simpl; trivial. Qed.